module module

`IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound`

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

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

IndisputableMonolith.Geometry.ReggeActionNonlinearCorrespondence module_import
IndisputableMonolith.Geometry.ReggeRemainderClosureAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.ReggeActionNonlinearHessianProof module_import

declarations in this module (55)

def NonlinearReggeCubicTaylorTheorem L28
def reggeActionCubicRemainderInput_of_taylorTheorem L32
theorem nonlinearReggeCubicTaylorTheorem_iff_localBound L42
theorem follows L48
theorem nonlinearReggeCubicTaylorTheorem_of_identically_zero L50
theorem canonicalRemainder_contDiffAt_zero_of_flatConfiguration L61
def CanonicalRemainderCubicTaylorFromJetInputsTarget L88
theorem nonlinearReggeCubicTaylorTheorem_of_remainderJetInputs L96
theorem linePotential_one L107
theorem linePotential_eq_smul L113
theorem norm_linePotential_le_of_mem_Icc_zero_one L119
def CanonicalRemainderLineCubicEstimateTarget L138
theorem nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate L146
theorem abs_value_le_cubic_of_taylor_data L155
def CanonicalRemainderLineTaylorDataTarget L186
def CanonicalRemainderLineContDiffTarget L206
theorem canonicalRemainderLineContDiff_of_flatConfiguration L216
def CanonicalRemainderLineQuadraticTaylorZeroTarget L250
def CanonicalRemainderLineThirdDerivBoundTarget L260
theorem min_pos3 L270
theorem lineTaylorData_of_splitTargets L274
theorem lineCubicEstimate_of_lineTaylorData L293
theorem nonlinearReggeCubicTaylorTheorem_of_lineTaylorData L309
def cubicRemainderInput_of_hessian_and_taylor L318
structure NonlinearReggeLocalHessianTaylorInputs L329
def nonlinearReggeLocalHessianTaylorInputs_of_hessian_and_taylor L336
def nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_taylor L350
def nonlinearReggeLocalHessianTaylorInputs_of_eventuallyZero_edgeStencil_and_remainderJetTarget L368
theorem canonicalRemainderLine_contDiffAt_zero_of_flatConfiguration L408
theorem canonicalRemainderLine_value_at_zero L436
theorem hasDerivAt_linePotential L445
theorem canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar L456
theorem iteratedDerivWithin_zero_canonicalRemainderLine L508
theorem zero_mem_Icc_zero_one L519
theorem iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs L525
theorem iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs L559
theorem canonicalRemainderLineQuadraticTaylorZero_of_jetInputs L605
theorem reggeActionRemainderSecondVariationInput_of_flat_directionalHessian L627
theorem canonicalRemainderLineQuadraticTaylorZero_of_flat_first_and_directionalHessian L637
def lineCLM L668
theorem lineCLM_apply L672
theorem lineCLM_eq_linePotential L677
theorem lineCLM_one L682
theorem canonicalRemainder_line_eq_comp L687
def CanonicalRemainderLineChainRuleBoundTarget L716
def CanonicalRemainderIteratedFDerivLocalBoundTarget L735
theorem canonicalRemainderLineThirdDerivBound_of_chainRule_and_localNorm L754
theorem canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration L798
theorem canonicalRemainderLineChainRuleBound_of_flatConfiguration L876
theorem canonicalRemainderLineThirdDerivBound_of_flatConfiguration L1061
theorem canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm L1072
theorem canonicalRemainderLineTaylorData_of_flat_and_remainderJets L1097
theorem nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets L1111
structure CanonicalRemainderAnalyticClosureCert L1130
def canonicalRemainderAnalyticClosureCert L1163