dAlembert_classification

formal source

 300Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
 301C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
 302ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/
 303theorem dAlembert_classification (H : ℝ → ℝ)
 304    (h_one : H 0 = 1) (h_cont : Continuous H)
 305    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
 306    (∀ x, H x = 1) ∨
 307    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
 308    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) := by
 309  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
 310  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
 311  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
 312  have h_H'0 : deriv H 0 = 0 :=
 313    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
 314  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
 315  set c := deriv (deriv H) 0 with hc_def
 316  have hDD : Differentiable ℝ (deriv H) := by
 317    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
 318    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
 319  by_cases hc_pos : 0 < c
 320  · -- c > 0: H = cosh(√c · t)
 321    right; left; refine ⟨Real.sqrt c, ?_⟩
 322    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
 323    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
 324    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
 325      have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
 326    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
 327      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
 328    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
 329      intro s
 330      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
 331        funext fun s => (hg_d s).deriv
 332      have h_dd_g : HasDerivAt (deriv g)
 333          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by