module module

`IndisputableMonolith.Cost.AczelTheorem`

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

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cost.AczelClassification module_import
IndisputableMonolith.Cost.AczelProof module_import
IndisputableMonolith.Cost.CauchyAuxiliary module_import
IndisputableMonolith.Cost.FunctionalEquationAczel module_import
IndisputableMonolith.Foundation.PolynomialityFromLogic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (20)

theorem dAlembert_even' L44
theorem dAlembert_locally_bounded L56
theorem dAlembert_double_angle L67
def H_AczelClassification L82
abbrev smooth L93
def Phi L95
lemma phi_zero L97
lemma phi_hasDerivAt L100
lemma phi_differentiable L105
lemma deriv_phi_eq L109
lemma exists_integral_ne_zero L112
lemma representation_formula L130
lemma phi_contDiff_succ L197
theorem dAlembert_contDiff_nat L206
theorem dAlembert_contDiff_smooth L224
theorem dAlembert_to_ODE_general L231
theorem ode_neg_zero_uniqueness L288
theorem ode_cos_uniqueness L315
theorem dAlembert_contDiff_top L353
theorem h_aczel_classification_proved L452