ode_regularity_continuous_of_smooth

formal source

1032  rw [lhs_eq, rhs_eq] at key; linarith
1033
1034/-- ODE regularity (3): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_continuous_hypothesis`. -/
1035theorem ode_regularity_continuous_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1036    ode_regularity_continuous_hypothesis H :=
1037  fun _ => h.continuous
1038
1039/-- ODE regularity (4): any H with ContDiff ℝ ⊤ satisfies `ode_regularity_differentiable_hypothesis`. -/
1040theorem ode_regularity_differentiable_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1041    ode_regularity_differentiable_hypothesis H :=
1042  fun _ _ => (h.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1043
1044/-- ODE regularity (5): any H with ContDiff ℝ ⊤ satisfies `ode_linear_regularity_bootstrap_hypothesis`. -/
1045theorem ode_regularity_bootstrap_of_smooth {H : ℝ → ℝ} (h : ContDiff ℝ ⊤ H) :
1046    ode_linear_regularity_bootstrap_hypothesis H :=
1047  fun _ _ _ => h.of_le le_top
1048
1049/-- **Theorem (d'Alembert → cosh, Aczél form)**: Using only the Aczél axiom, a continuous
1050    solution to d'Alembert with H(0) = 1 and H''(0) = 1 must equal cosh.
1051
1052    This is the clean version of `dAlembert_cosh_solution`, requiring no regularity params. -/
1053theorem dAlembert_cosh_solution_aczel
1054    [AczelSmoothnessPackage]
1055    (H : ℝ → ℝ)
1056    (h_one : H 0 = 1)
1057    (h_cont : Continuous H)
1058    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u)
1059    (h_d2_zero : deriv (deriv H) 0 = 1) :
1060    ∀ t, H t = Real.cosh t := by
1061  have h_smooth : ContDiff ℝ ⊤ H := aczel_dAlembert_smooth H h_one h_cont h_dAlembert
1062  have hDiff : Differentiable ℝ H :=
1063    (h_smooth.of_le le_top : ContDiff ℝ 1 H).differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
1064  have h_even : Function.Even H := dAlembert_even H h_one h_dAlembert
1065  have h_H'0 : deriv H 0 = 0 := even_deriv_at_zero H h_even hDiff.differentiableAt