dAlembert_contDiff_top

formal source

 350
 351/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
 352    implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/
 353private theorem dAlembert_contDiff_top (H : ℝ → ℝ)
 354    (h_one : H 0 = 1) (h_cont : Continuous H)
 355    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 356    ContDiff ℝ ⊤ H := by
 357  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
 358  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
 359  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 360  have h_H'0 : deriv H 0 = 0 :=
 361    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
 362  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
 363  set c := deriv (deriv H) 0
 364  have hDD : Differentiable ℝ (deriv H) := by
 365    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
 366    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable
 367      (by decide : (1 : WithTop ℕ∞) ≠ 0)
 368  by_cases hc_pos : 0 < c
 369  · -- Case c > 0: H = cosh(√c · t)
 370    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
 371    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
 372    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
 373      have := (hasDerivAt_id s).div_const (Real.sqrt c)
 374      simp only [id, one_div] at this; exact this
 375    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
 376      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 377    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
 378      intro s
 379      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
 380        funext fun s => (hg_d s).deriv
 381      have h_dd_g : HasDerivAt (deriv g)
 382          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
 383        rw [hg1]