def
definition
ode_linear_regularity_bootstrap_hypothesis_neg
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation on GitHub at line 191.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
188deriv (deriv f) t = -f t holds pointwise), then f is automatically C².
189
190This is a standard result: linear ODEs with smooth coefficients have smooth solutions. -/
191def ode_linear_regularity_bootstrap_hypothesis_neg (H : ℝ → ℝ) : Prop :=
192 (∀ t, deriv (deriv H) t = -H t) → Continuous H → Differentiable ℝ H → ContDiff ℝ 2 H
193
194/-- **ODE regularity: continuous solutions.** -/
195def ode_regularity_continuous_hypothesis_neg (H : ℝ → ℝ) : Prop :=
196 (∀ t, deriv (deriv H) t = -H t) → Continuous H
197
198/-- **ODE regularity: differentiable solutions.** -/
199def ode_regularity_differentiable_hypothesis_neg (H : ℝ → ℝ) : Prop :=
200 (∀ t, deriv (deriv H) t = -H t) → Continuous H → Differentiable ℝ H
201
202/-- cos satisfies the ODE regularity bootstrap. -/
203theorem cos_satisfies_bootstrap_neg : ode_linear_regularity_bootstrap_hypothesis_neg Real.cos := by
204 intro _ _ _
205 exact Real.contDiff_cos
206
207/-- cos is continuous. -/
208theorem cos_satisfies_continuous_neg : ode_regularity_continuous_hypothesis_neg Real.cos := by
209 intro _
210 exact Real.continuous_cos
211
212/-- cos is differentiable. -/
213theorem cos_satisfies_differentiable_neg : ode_regularity_differentiable_hypothesis_neg Real.cos := by
214 intro _ _
215 exact Real.differentiable_cos
216
217/-- ODE cosine uniqueness with regularity hypotheses. -/
218theorem ode_cos_uniqueness (H : ℝ → ℝ)
219 (h_ODE : ∀ t, deriv (deriv H) t = -H t)
220 (h_H0 : H 0 = 1)
221 (h_H'0 : deriv H 0 = 0)