phi_contDiff_succ

formal source

 136    linarith
 137  field_simp at h_integral ⊢; linarith
 138
 139private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
 140    (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by
 141  suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
 142  rw [contDiff_succ_iff_deriv]
 143  exact ⟨phi_differentiable H h_cont,
 144    fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
 145    by rwa [deriv_phi_eq H h_cont]⟩
 146
 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
 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
 165private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
 166    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 167    ContDiff ℝ smooth H :=
 168  contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
 169