dAlembert_to_ODE_of_contDiff

formal source

 117  linarith
 118
 119/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/
 120theorem dAlembert_to_ODE_of_contDiff
 121    (Hf : ℝ → ℝ)
 122    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
 123    (h_diff : ContDiff ℝ 2 Hf)
 124    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
 125    ∀ t, deriv (deriv Hf) t = Hf t := by
 126  intro t
 127  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
 128  rw [h_deriv2_zero] at h_rel
 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