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
proof body
Term-mode proof.
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
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.