Jcost_weak_triangle_FALSE

formal source

 489    - 49.005 > 24.3
 490
 491    Use `Jcost_submult` instead: J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y), which IS proved. -/
 492theorem Jcost_weak_triangle_FALSE :
 493    ¬ (∀ x y : ℝ, 0 < x → 0 < y →
 494      Jcost (x * y) ≤ 2 * (Jcost x + Jcost y) + 2 * Real.sqrt (Jcost x * Jcost y)) := by
 495  intro h
 496  -- Counterexample: x = y = 10, J(100) > 2(J(10)+J(10)) + 2*sqrt(J(10)*J(10))
 497  -- J(100) = (100 + 1/100)/2 - 1 = 49.005
 498  -- J(10) = (10 + 0.1)/2 - 1 = 4.05
 499  -- RHS = 2*(4.05 + 4.05) + 2*sqrt(4.05*4.05) = 16.2 + 8.1 = 24.3
 500  -- 49.005 > 24.3 is TRUE, not ≤, so the inequality fails
 501  have hc := h 10 10 (by norm_num) (by norm_num)
 502  -- The claim asserts ≤ but the counterexample shows >
 503  -- J(100) = 49.005, RHS = 24.3, so 49.005 > 24.3
 504  simp only [Jcost] at hc
 505  nlinarith [sq_nonneg (10 : ℝ), Real.sqrt_nonneg (Jcost 10 * Jcost 10)]
 506
 507/-- The d'Alembert identity: J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y) -/
 508theorem dalembert_identity {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 509    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by
 510  have hx0 : x ≠ 0 := ne_of_gt hx
 511  have hy0 : y ≠ 0 := ne_of_gt hy
 512  have hxy : x * y ≠ 0 := mul_ne_zero hx0 hy0
 513  have hxdy : x / y ≠ 0 := div_ne_zero hx0 hy0
 514  simp only [Jcost_eq_sq hxy, Jcost_eq_sq hxdy, Jcost_eq_sq hx0, Jcost_eq_sq hy0]
 515  field_simp
 516  ring
 517
 518/-- From d'Alembert: J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y) since J(x/y) ≥ 0 -/
 519lemma Jcost_submult {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 520    Jcost (x * y) ≤ 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by
 521  have h := dalembert_identity hx hy
 522  have hnonneg : 0 ≤ Jcost (x / y) := Jcost_nonneg (div_pos hx hy)