theorem
proved
cos_satisfies_bootstrap_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 203.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
222 (h_cont_hyp : ode_regularity_continuous_hypothesis_neg H)
223 (h_diff_hyp : ode_regularity_differentiable_hypothesis_neg H)
224 (h_bootstrap_hyp : ode_linear_regularity_bootstrap_hypothesis_neg H) :
225 ∀ t, H t = Real.cos t := by
226 have h_cont : Continuous H := h_cont_hyp h_ODE
227 have h_diff : Differentiable ℝ H := h_diff_hyp h_ODE h_cont
228 have h_C2 : ContDiff ℝ 2 H := h_bootstrap_hyp h_ODE h_cont h_diff
229 exact ode_cos_uniqueness_contdiff H h_C2 h_ODE h_H0 h_H'0
230
231/-! ## Part 3: d'Alembert Functional Equation → Cosine
232
233The d'Alembert equation H(t+u) + H(t-u) = 2H(t)H(u) with H(0) = 1 has two branches: