module module

`IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (23)

theorem ode_neg_energy_constant L62
theorem ode_zero_uniqueness_neg L102
theorem cos_second_deriv_eq L118
theorem cos_initials L130
theorem ode_cos_uniqueness_contdiff L137
def ode_linear_regularity_bootstrap_hypothesis_neg L191
def ode_regularity_continuous_hypothesis_neg L195
def ode_regularity_differentiable_hypothesis_neg L199
theorem cos_satisfies_bootstrap_neg L203
theorem cos_satisfies_continuous_neg L208
theorem cos_satisfies_differentiable_neg L213
theorem ode_cos_uniqueness L218
def dAlembert_continuous_implies_smooth_hypothesis_neg L242
def dAlembert_to_ODE_hypothesis_neg L249
theorem cos_dAlembert_smooth L254
theorem cos_dAlembert_to_ODE L259
theorem cos_dAlembert L264
theorem dAlembert_cos_solution L275
structure AngleCouplingAxioms L312
structure AngleStandardRegularity L325
theorem THEOREM_angle_coupling_rigidity L338
theorem cos_satisfies_axioms L355
theorem cos_satisfies_regularity L365