module module

`IndisputableMonolith.Foundation.DAlembert.Stability`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (24)

def dAlembertDefect L57
lemma defect_zero_iff_dAlembert L61
lemma defect_even_in_t L66
lemma defect_even_in_u L83
lemma defect_symmetric L97
def UniformDefectBound L110
structure StabilityHypotheses L114
structure StabilityBounds L129
def optimal_h L171
def StabilityEstimate L191
def ODEApproximation L201
def ODEApproximationHypothesis L221
theorem ode_approximation_from_defect L225
def StabilityFromODEHypothesis L242
theorem stability_from_ode_approx L246
theorem dAlembert_stability L254
def CostStabilityEstimate L273
def CostStabilityTransferHypothesis L278
theorem cost_stability_transfer L287
theorem stability_calibrated L301
theorem cost_stability_calibrated L315
def ZeroDefectImpliesCoshHypothesis L342
theorem zero_defect_implies_cosh L347
theorem zero_defect_calibrated_implies_cosh L355