module
module
IndisputableMonolith.Geometry.ReggeRemainderClosureAudit
show as:
view Lean formalization →
depends on (2)
declarations in this module (7)
-
structure
RemainderAnalyticClosed -
def
remainderAnalyticClosed -
theorem
canonicalRemainderLineThirdDerivBound_closed -
theorem
nonlinearReggeCubicTaylorTheorem_closed -
theorem
nonlinearReggeLocalHessianTaylorInputs_closed -
theorem
nonlinearReggeJCostLocalCorrespondence_closed -
theorem
strongestTrueReggeJCostReplacement_closed