theorem
proved
term proof
Jcost_weak_triangle_FALSE
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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) -/