theorem
proved
tactic proof
composition_law_equiv_coshAdd
show as:
view Lean formalization →
formal statement (Lean)
719theorem composition_law_equiv_coshAdd (F : ℝ → ℝ) :
720 SatisfiesCompositionLaw F ↔ CoshAddIdentity F := by
proof body
Tactic-mode proof.
721 constructor
722 · intro hComp t u
723 have hexp_t_pos : 0 < Real.exp t := Real.exp_pos t
724 have hexp_u_pos : 0 < Real.exp u := Real.exp_pos u
725 have h := hComp (Real.exp t) (Real.exp u) hexp_t_pos hexp_u_pos
726 -- exp(t) * exp(u) = exp(t + u)
727 have h1 : Real.exp t * Real.exp u = Real.exp (t + u) := (Real.exp_add t u).symm
728 -- exp(t) / exp(u) = exp(t - u)
729 have h2 : Real.exp t / Real.exp u = Real.exp (t - u) := by
730 rw [div_eq_mul_inv, ← Real.exp_neg u, ← Real.exp_add, sub_eq_add_neg]
731 simp only [G, h1, h2] at h ⊢
732 linarith
733 · intro hCosh x y hx hy
734 let t := Real.log x
735 let u := Real.log y
736 have hx_eq : x = Real.exp t := (Real.exp_log hx).symm
737 have hy_eq : y = Real.exp u := (Real.exp_log hy).symm
738 have h := hCosh t u
739 simp only [G] at h
740 rw [hx_eq, hy_eq]
741 rw [← Real.exp_add, ← Real.exp_sub]
742 -- h : F (exp (t + u)) + F (exp (t - u)) = 2 * (F (exp t) * F (exp u)) + 2 * (F (exp t) + F (exp u))
743 -- Goal: F (exp (t + u)) + F (exp (t - u)) = 2 * F (exp t) * F (exp u) + 2 * F (exp t) + 2 * F (exp u)
744 calc F (Real.exp (t + u)) + F (Real.exp (t - u))
745 = 2 * (F (Real.exp t) * F (Real.exp u)) + 2 * (F (Real.exp t) + F (Real.exp u)) := h
746 _ = 2 * F (Real.exp t) * F (Real.exp u) + 2 * F (Real.exp t) + 2 * F (Real.exp u) := by ring
747
748/-- **Theorem 1.1 (Main Result, Reformulated)**:
749
750Let F : ℝ₊ → ℝ satisfy:
7511. Reciprocity: F(x) = F(1/x)
7522. Normalization: F(1) = 0
7533. Composition Law: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
7544. Calibration: lim_{t→0} 2F(e^t)/t² = 1
7555. Continuity and regularity hypotheses
756
757Then F = J on ℝ₊, where J(x) = (x + 1/x)/2 - 1.
758
759This theorem corresponds to Theorem 1.1 in:
760 J. Washburn & M. Zlatanović, "Uniqueness of the Canonical Reciprocal Cost" -/