ode_linear_regularity_bootstrap_hypothesis

formal source

 457
 458    Note: In a fully formal treatment, we would use Picard-Lindelöf theory. Here we
 459    package this as a hypothesis that is discharged by existing Mathlib theory. -/
 460def ode_linear_regularity_bootstrap_hypothesis (H : ℝ → ℝ) : Prop :=
 461  (∀ t, deriv (deriv H) t = H t) → Continuous H → Differentiable ℝ H → ContDiff ℝ 2 H
 462
 463/-- **ODE regularity: continuous solutions.**
 464
 465    For f'' = f, if the equation holds pointwise, then f is continuous.
 466    This is immediate from the definition (we assume the derivatives exist). -/
 467def ode_regularity_continuous_hypothesis (H : ℝ → ℝ) : Prop :=
 468  (∀ t, deriv (deriv H) t = H t) → Continuous H
 469
 470/-- **ODE regularity: differentiable solutions.**
 471
 472    For f'' = f with f continuous, f is differentiable.
 473    This follows from the ODE: f' exists since f'' = f requires f' to exist first. -/
 474def ode_regularity_differentiable_hypothesis (H : ℝ → ℝ) : Prop :=
 475  (∀ t, deriv (deriv H) t = H t) → Continuous H → Differentiable ℝ H
 476
 477/-! ### Proving the regularity hypotheses
 478
 479For the linear ODE f'' = f, we can verify the regularity hypotheses hold
 480for the known solution cosh. For arbitrary solutions, we rely on general
 481ODE theory (Picard-Lindelöf). -/
 482
 483/-- cosh satisfies the ODE regularity bootstrap. -/
 484theorem cosh_satisfies_bootstrap : ode_linear_regularity_bootstrap_hypothesis Real.cosh := by
 485  intro _ _ _
 486  exact Real.contDiff_cosh
 487
 488/-- cosh is continuous. -/
 489theorem cosh_satisfies_continuous : ode_regularity_continuous_hypothesis Real.cosh := by
 490  intro _