sqrt_triangle_violation

proof body

Tactic-mode proof.

 448  have h1 : 0 ≤ Real.sqrt (1 / 2) + Real.sqrt (4 / 3) := by positivity
 449  change Real.sqrt (1 / 2) + Real.sqrt (4 / 3) < Real.sqrt (25 / 6)
 450  rw [← Real.sqrt_sq h1]
 451  rw [Real.sqrt_lt_sqrt_iff (by positivity)]
 452  rw [add_sq, Real.sq_sqrt (by norm_num), Real.sq_sqrt (by norm_num)]
 453  rw [mul_assoc, ← Real.sqrt_mul (by norm_num)]
 454  norm_num
 455  -- Goal: 1 / 2 + 2 * (√2 / √3) + 4 / 3 < 25 / 6
 456  suffices 2 * (Real.sqrt 2 / Real.sqrt 3) < 7 / 3 by linarith
 457  have h_lhs : 2 * (Real.sqrt 2 / Real.sqrt 3) = Real.sqrt (8 / 3) := by
 458    rw [← Real.sqrt_div (by norm_num) 3]
 459    rw [show (2 : ℝ) = Real.sqrt 4 by norm_num]
 460    rw [← Real.sqrt_mul (by norm_num)]
 461    norm_num
 462  have h_rhs : (7 / 3 : ℝ) = Real.sqrt (49 / 9) := by
 463    rw [Real.sqrt_div (by norm_num) 9]
 464    norm_num
 465  rw [h_lhs, h_rhs]
 466  rw [Real.sqrt_lt_sqrt_iff (by positivity)]
 467  norm_num
 468
 469/-- **DEPRECATED**: The naive triangle inequality does NOT hold for Jmetric.
 470    Use `Jcost_submult` instead, which gives a valid submultiplicativity bound. -/