`cos_satisfies_regularity`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation
domain: Measurement
line: 365 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation on GitHub at line 365.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 362    simp [Real.cos_zero]
 363
 364/-- cos satisfies standard regularity. -/
 365theorem cos_satisfies_regularity : AngleStandardRegularity Real.cos where
 366  smooth := cos_dAlembert_smooth
 367  ode := cos_dAlembert_to_ODE
 368  cont := cos_satisfies_continuous_neg
 369  diff := cos_satisfies_differentiable_neg
 370  boot := cos_satisfies_bootstrap_neg
 371
 372end AngleFunctionalEquation
 373end RecognitionAngle
 374end Measurement
 375end IndisputableMonolith

papers checked against this theorem

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