Jmetric

formal source

 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)
 360  -- h : cosh(2*(t/2)) = cosh²(t/2) + sinh²(t/2)
 361  simp only [two_mul, add_halves] at h
 362  -- So h : cosh(t) = cosh²(t/2) + sinh²(t/2)
 363  -- From cosh²(t/2) - sinh²(t/2) = 1, we get cosh²(t/2) = 1 + sinh²(t/2)
 364  have h2 := Real.cosh_sq_sub_sinh_sq (t / 2)
 365  have h3 : Real.cosh (t / 2) ^ 2 = 1 + Real.sinh (t / 2) ^ 2 := by linarith
 366  -- Substitute: cosh(t) = (1 + sinh²(t/2)) + sinh²(t/2) = 1 + 2sinh²(t/2)
 367  -- So cosh(t) - 1 = 2sinh²(t/2)
 368  calc 2 * (Real.cosh t - 1)
 369      = 2 * ((Real.cosh (t / 2) ^ 2 + Real.sinh (t / 2) ^ 2) - 1) := by rw [h]