IndisputableMonolith.Geometry.ReggeActionSecondVariation

declarations in this module (18)

• def linePotential L27
• theorem linePotential_zero L31
• def HasSecondDerivAt L39
• theorem hessianQuadratic_linePotential L42
• theorem hessianQuadratic_along_line_hasSecondDerivAt_zero L56
• def actionAlongLine L86
• def CanonicalHessianSecondVariationAtZero L93
• structure ReggeActionSecondVariationInput L100
• def reggeActionSecondVariationInput_of_directionalSecondVariation L105
• theorem reggeAction_secondVariation_eq_canonicalHessian L114
• def CanonicalRemainderSecondVariationZero L123
• structure ReggeActionRemainderSecondVariationInput L132
• theorem reggeActionRemainder_secondVariation_zero L137
• def LocalCubicRemainderBound L144
• structure ReggeActionCubicRemainderInput L153
• def reggeActionCubicRemainderInput_of_bound L158
• def reggeActionCubicRemainderInput_of_identically_zero L167
• theorem reggeActionRemainder_cubic_bound L181