lemma
proved
Jcost_zero_iff_one
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost on GitHub at line 329.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
Jcost_eq_zero_iff -
of -
of -
of -
for -
Jcost_zero_iff_one -
Triangle -
Jcost_zero_iff_one -
of -
Jcost_eq_zero_iff
used by
formal source
326 simpa [Jlog_zero] using Jlog_nonneg t
327
328/-- From J(x) = 0 and x > 0, conclude x = 1. -/
329lemma Jcost_zero_iff_one {x : ℝ} (hx : 0 < x) (h : Jcost x = 0) : x = 1 :=
330 (Jcost_eq_zero_iff x hx).mp h
331
332/-! ## Triangle Inequality for J -/
333
334/-- J in terms of cosh: J(exp(t)) = cosh(t) - 1 -/
335lemma Jcost_exp_cosh (t : ℝ) : Jcost (Real.exp t) = Real.cosh t - 1 :=
336 Jlog_as_cosh t
337
338/-- The sqrt of 2*J gives |log|, which IS a metric. -/
339noncomputable def Jmetric (x : ℝ) : ℝ := Real.sqrt (2 * Jcost x)
340
341/-- Jmetric(1) = 0 -/
342lemma Jmetric_one : Jmetric 1 = 0 := by
343 simp [Jmetric, Jcost_unit0]
344
345/-- Jmetric is symmetric: Jmetric(x) = Jmetric(1/x) -/
346lemma Jmetric_symm {x : ℝ} (hx : 0 < x) : Jmetric x = Jmetric x⁻¹ := by
347 simp only [Jmetric, Jcost_symm hx]
348
349/-- Jmetric is non-negative -/
350lemma Jmetric_nonneg {x : ℝ} (_ : 0 < x) : 0 ≤ Jmetric x :=
351 Real.sqrt_nonneg _
352
353/-- Key identity: 2(cosh(t) - 1) = 4sinh²(t/2)
354
355 Proof: cosh(2u) = cosh²(u) + sinh²(u), and cosh²(u) = 1 + sinh²(u).
356 So cosh(2u) = 1 + 2sinh²(u), hence cosh(2u) - 1 = 2sinh²(u). -/
357lemma cosh_minus_one_eq (t : ℝ) : 2 * (Real.cosh t - 1) = 4 * Real.sinh (t / 2) ^ 2 := by
358 -- Use the double-angle formula: cosh(2u) = cosh²(u) + sinh²(u)
359 have h := Real.cosh_two_mul (t / 2)