pith. machine review for the scientific record. sign in
lemma proved term proof

Jmetric_exp_sinh

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 414lemma Jmetric_exp_sinh (t : ℝ) : Jmetric (Real.exp t) = 2 * |Real.sinh (t / 2)| := by

proof body

Term-mode proof.

 415  unfold Jmetric
 416  rw [Jcost_exp_cosh, cosh_minus_one_eq]
 417  -- sqrt(4 * sinh²(t/2)) = sqrt(4) * |sinh(t/2)| = 2 * |sinh(t/2)|
 418  rw [show (4 : ℝ) * Real.sinh (t / 2) ^ 2 = (2 * Real.sinh (t / 2)) ^ 2 by ring]
 419  rw [Real.sqrt_sq_eq_abs]
 420  rw [abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 2)]
 421
 422/-! ### Note on Triangle Inequality
 423
 424The function `Jmetric(x) = sqrt(2 * Jcost(x))` does NOT satisfy the triangle inequality
 425under multiplication. Numerical counterexample:
 426- Jmetric(6) ≈ 2.04 > Jmetric(2) + Jmetric(3) ≈ 1.86
 427
 428This is expected: J-cost measures the "recognition strain" of a ratio, and strain
 429compounds superlinearly when multiplying far-from-unity ratios.
 430
 431The key inequality that DOES hold is the d'Alembert identity, which gives
 432`Jcost_submult`: J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y). -/
 433
 434/-- **Standard Analysis**: Evaluation of Jmetric at specific points. -/

depends on (21)

Lean names referenced from this declaration's body.