dAlembert_contDiff_smooth

formal source

 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)
 237  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
 238    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
 239    rw [contDiff_succ_iff_deriv] at h2; exact h2.2.2
 240  have hDiffDeriv : Differentiable ℝ (deriv H) :=
 241    hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 242  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
 243    have h := (hasDerivAt_id v).add_const s; simp only [id] at h
 244    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
 245  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
 246    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
 247      have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
 248    have h2 := h1.const_add s
 249    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
 250  intro t
 251  have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
 252    funext (h_dAl t)
 253  have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
 254             deriv (deriv (fun u => 2 * H t * H u)) 0 :=