dAlembert_to_ODE_hypothesis_of_contDiff

formal source

 129  linarith
 130
 131/-- Bridge from an explicit `ContDiff ℝ 2` hypothesis to the legacy ODE hypothesis. -/
 132theorem dAlembert_to_ODE_hypothesis_of_contDiff
 133    (Hf : ℝ → ℝ) (h_diff : ContDiff ℝ 2 Hf) :
 134    dAlembert_to_ODE_hypothesis Hf := by
 135  intro _ _ h_dAlembert h_deriv2_zero
 136  exact dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
 137
 138/-- A normalized composition-law cost is automatically reciprocal. -/
 139theorem composition_law_forces_reciprocity
 140    (F : ℝ → ℝ)
 141    (hNorm : IsNormalized F)
 142    (hComp : SatisfiesCompositionLaw F) :
 143    IsReciprocalCost F := by
 144  intro x hx
 145  let Hf : ℝ → ℝ := H F
 146  have h_H0 : Hf 0 = 1 := by
 147    dsimp [Hf]
 148    simpa [H, G, IsNormalized] using hNorm
 149  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
 150  have h_direct : DirectCoshAdd (G F) := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
 151  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
 152    intro t u
 153    have hG := h_direct t u
 154    have h_goal :
 155        (G F (t + u) + 1) + (G F (t - u) + 1) = 2 * (G F t + 1) * (G F u + 1) := by
 156      calc
 157        (G F (t + u) + 1) + (G F (t - u) + 1)
 158            = (G F (t + u) + G F (t - u)) + 2 := by ring
 159        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
 160        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
 161    simpa [Hf, H] using h_goal
 162  have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert