147private theorem dAlembert_contDiff_nat (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H) 148 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) : 149 ∀ n : ℕ, ContDiff ℝ (n : ℕ∞) H := by
proof body
Term-mode proof.
150 obtain ⟨δ, _, hδ_ne⟩ := exists_integral_ne_zero H h_one h_cont 151 have h_rep := representation_formula H h_cont h_dAl hδ_ne 152 intro n; induction n with 153 | zero => exact contDiff_zero.mpr h_cont 154 | succ n ih => 155 have h_phi := phi_contDiff_succ H h_cont ih 156 have h1 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t + δ)) := 157 h_phi.comp (contDiff_id.add contDiff_const) 158 have h2 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (fun t => Phi H (t - δ)) := 159 h_phi.comp (contDiff_id.sub contDiff_const) 160 have h4 : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) 161 (fun t => (Phi H (t + δ) - Phi H (t - δ)) / (2 * Phi H δ)) := 162 (h1.sub h2).div_const _ 163 exact (funext h_rep) ▸ h4 164
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.