`ode_regularity_differentiable_hypothesis`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.FunctionalEquation
domain: Cost
line: 474 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 474.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 498theorem ode_cosh_uniqueness (H : ℝ → ℝ)
 499    (h_ODE : ∀ t, deriv (deriv H) t = H t)
 500    (h_H0 : H 0 = 1)
 501    (h_H'0 : deriv H 0 = 0)
 502    (h_cont_hyp : ode_regularity_continuous_hypothesis H)
 503    (h_diff_hyp : ode_regularity_differentiable_hypothesis H)
 504    (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis H) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.