reciprocal_implies_G_even

formal source

 702    F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
 703
 704/-- **Lemma 2.1**: If F is reciprocal, then G(t) = F(e^t) is even. -/
 705theorem reciprocal_implies_G_even (F : ℝ → ℝ) (hRecip : IsReciprocalCost F) :
 706    Function.Even (G F) :=
 707  G_even_of_reciprocal_symmetry F (fun {x} hx => hRecip x hx)
 708
 709/-- **Lemma**: If F is normalized, then G(0) = 0. -/
 710theorem normalized_implies_G_zero (F : ℝ → ℝ) (hNorm : IsNormalized F) :
 711    G F 0 = 0 :=
 712  G_zero_of_unit F hNorm
 713
 714/-- **Key Identity**: The composition law on F is equivalent to CoshAddIdentity on G.
 715
 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