ode_regularity_differentiable_of_smooth

formal source

 135  fun _ => h.continuous
 136
 137/-- ODE regularity (4): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_differentiable_hypothesis`. -/
 138theorem ode_regularity_differentiable_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 139    ode_regularity_differentiable_hypothesis H :=
 140  fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable
 141    (by decide : (1 : WithTop ℕ∞) ≠ 0)
 142
 143/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
 144theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
 145    ode_linear_regularity_bootstrap_hypothesis H :=
 146  fun _ _ _ => h.of_le le_top
 147
 148/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
 149    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
 150
 151    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
 152theorem dAlembert_cosh_solution_aczel
 153    (H : ℝ → ℝ)
 154    (h_one : H 0 = 1)
 155    (h_cont : Continuous H)
 156    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
 157    (h_d2_zero : deriv (deriv H) 0 = 1) :
 158    ∀ t, H t = Real.cosh t := by
 159  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
 160  have hDiff : Differentiable ℝ H :=
 161    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable
 162      (by decide : (1 : WithTop ℕ∞) ≠ 0)
 163  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
 164  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt
 165  have h_ode : ∀ t, deriv (deriv H) t = H t :=
 166    dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
 167  have h_C2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
 168  exact ode_cosh_uniqueness_contdiff H h_C2 h_ode h_one h_H'0