ode_regularity_continuous_hypothesis

formal source

 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 _
 491  exact Real.continuous_cosh
 492
 493/-- cosh is differentiable. -/
 494theorem cosh_satisfies_differentiable : ode_regularity_differentiable_hypothesis Real.cosh := by
 495  intro _ _
 496  exact Real.differentiable_cosh
 497