composition_law_equiv_coshAdd

formal source

 716Specifically: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
 717becomes: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
 718via the substitution x = e^s, y = e^t. -/
 719theorem composition_law_equiv_coshAdd (F : ℝ → ℝ) :
 720    SatisfiesCompositionLaw F ↔ CoshAddIdentity F := by
 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