dAlembert_classification

formal source

 169    For λ ≠ 0, define K(s) = H(s/λ); then K'' = K, K(0)=1, K'(0)=0, so K = cosh,
 170    hence H(t) = cosh(λt). For λ = 0, H'' = 0 gives H = 1 = cosh(0).
 171    Formalizing the scaling argument requires careful chain-rule handling. -/
 172theorem dAlembert_classification :
 173    ∀ H : ℝ → ℝ, ∀ lam : ℝ,
 174    SatisfiesDAlembert H →
 175    ContDiff ℝ 2 H →
 176    deriv H 0 = 0 →
 177    deriv (deriv H) 0 = lam ^ 2 →
 178    ∀ t, H t = Real.cosh (lam * t) := by
 179  intro H lam hDA hSmooth hDeriv0 hCalib t
 180  have h_ode : ∀ x, deriv (deriv H) x = deriv (deriv H) 0 * H x :=
 181    dalembert_deriv_ode H hSmooth hDA.2
 182  by_cases hlam : lam = 0
 183  · -- λ = 0: H'' = 0, so H is constant; H(0)=1, H'(0)=0 ⇒ H = 1 = cosh(0)
 184    subst hlam
 185    have hode0 : ∀ x, deriv (deriv H) x = 0 := fun x => by
 186      rw [h_ode x, hCalib, zero_pow two_ne_zero]; exact zero_mul (H x)
 187    -- H''=0 ⇒ deriv H constant; deriv H 0 = 0 ⇒ deriv H = 0 ⇒ H constant; H 0 = 1 ⇒ H = 1
 188    have hd_deriv : Differentiable ℝ (deriv H) := hSmooth.differentiable_deriv_two
 189    have hH'0 : ∀ x, deriv H x = 0 := fun x => (is_const_of_deriv_eq_zero hd_deriv hode0 x 0).trans hDeriv0
 190    have hH_const : ∀ x, H x = 1 := fun x => (is_const_of_deriv_eq_zero (hSmooth.differentiable (by decide)) hH'0 x 0).trans hDA.1
 191    simp only [hH_const t, zero_mul, Real.cosh_zero]
 192  · -- λ ≠ 0: K(s) = H(s/λ) satisfies K'' = K, K(0)=1, K'(0)=0, K''(0)=1; apply unit calibration.
 193    let K := fun s => H (s / lam)
 194    have hK0 : K 0 = 1 := by simp [K, hDA.1]
 195    have hK_DA : SatisfiesDAlembert K := by
 196      constructor; exact hK0
 197      intro t u
 198      simp only [K]
 199      have ht : (t + u) / lam = t / lam + u / lam := by field_simp [hlam]
 200      have ht' : (t - u) / lam = t / lam - u / lam := by field_simp [hlam]
 201      rw [ht, ht']
 202      exact hDA.2 (t / lam) (u / lam)