sqrt_triangle_violation

formal source

 444  unfold Jmetric Jcost
 445  norm_num
 446
 447theorem sqrt_triangle_violation : Real.sqrt (25 / 6) > Real.sqrt (1 / 2) + Real.sqrt (4 / 3) := by
 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. -/
 471theorem Jmetric_triangle_FALSE {x y : ℝ} (_hx : 0 < x) (_hy : 0 < y) :
 472    ¬ (∀ a b : ℝ, 0 < a → 0 < b → Jmetric (a * b) ≤ Jmetric a + Jmetric b) := by
 473  intro h
 474  -- Counterexample: a = 2, b = 3
 475  let a : ℝ := 2
 476  let b : ℝ := 3
 477  have ha : 0 < a := by norm_num