dAlembert_contDiff_nat

formal source

 203    by rwa [deriv_phi_eq H h_cont]⟩
 204
 205/-- Core bootstrap: continuous d'Alembert → C^n for all n. -/
 206private theorem dAlembert_contDiff_nat (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
 207    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 208    ∀ n : ℕ, ContDiff ℝ (n : ℕ∞) H := by
 209  obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_cont
 210  have h_rep := representation_formula H h_cont h_dAl hδ_ne
 211  intro n; induction n with
 212  | zero => exact contDiff_zero.mpr h_cont
 213  | succ n ih =>
 214    have h_phi := phi_contDiff_succ H h_cont ih
 215    have h1 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t + δ)) :=
 216      h_phi.comp (contDiff_id.add contDiff_const)
 217    have h2 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t - δ)) :=
 218      h_phi.comp (contDiff_id.sub contDiff_const)
 219    have h4 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞)
 220        (fun t => (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ)) :=
 221      (h1.sub h2).div_const _
 222    exact (funext h_rep) ▸ h4
 223
 224private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
 225    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 226    ContDiff ℝ smooth H :=
 227  contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
 228
 229/-! ## §4 General ODE Derivation: C^∞ + d'Alembert → H'' = c·H -/
 230
 231private theorem dAlembert_to_ODE_general (H : ℝ → ℝ)
 232    (h_smooth : ContDiff ℝ smooth H)
 233    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 234    ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
 235  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_smooth) 2
 236  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)