module module

`IndisputableMonolith.Geometry.ReggeActionNonlinearHessianProof`

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

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

IndisputableMonolith.Geometry.ReggeActionCubicTaylorBound module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.ReggeActionSecondVariation module_import

declarations in this module (142)

theorem differentiableAt_eventually_of_contDiffAt_top L28
theorem deriv_differentiableAt_of_contDiffAt_top L40
theorem hasSecondDerivAt_const_add L53
def NonlinearReggeDirectionalHessianTheorem L67
def ActionDerivativeLinearizationNearZeroTarget L78
def ActionDerivativeFirstOrderTangencyTarget L88
theorem nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency L97
theorem nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero L118
theorem actionDerivativeFirstOrderTangency_of_linearizationNearZero L132
def canonicalQuadraticAlongLine L145
def canonicalRemainderAlongLine L152
theorem actionAlongLine_canonical_split L162
theorem canonicalRemainderAlongLine_eq_action_sub_quadratic L179
theorem canonicalQuadraticAlongLine_hasSecondDerivAt_zero L194
theorem canonicalQuadraticAlongLine_differentiableAt L208
theorem canonicalQuadraticAlongLine_hasDerivAt L224
theorem deriv_canonicalQuadraticAlongLine L242
def ActionDerivativeTangencyToQuadraticTarget L251
theorem actionDerivativeFirstOrderTangency_of_quadraticTangency L260
def hingeLineDeriv L273
def deficitLineDeriv L282
def hingeLineSecondDeriv L289
def deficitLineSecondDeriv L296
def reggeActionProductRuleDerivative L304
def reggeActionSecondProductRuleDerivative L315
def ActionDerivativeProductRuleNearZeroTarget L328
def HingeDeficitLineDifferentiabilityNearZeroTarget L336
def HingeDeficitSecondLineDifferentiabilityAtZeroTarget L348
theorem hingeLineDeriv_differentiableAt_zero L354
def DeficitSecondLineDifferentiabilityAtZeroTarget L396
theorem hingeDeficitSecondLineDifferentiability_of_deficit L401
theorem hingeLine_contDiffAt_zero L408
theorem deficitLine_contDiffAt_zero_of_flatConfiguration L426
theorem deficitLineDeriv_differentiableAt_zero_of_flatConfiguration L446
theorem hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration L456
theorem hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration L464
theorem actionDerivativeProductRuleNearZero_of_factorDifferentiability L482
theorem actionDerivativeProductRuleNearZero_of_flatConfiguration L534
theorem productRule_hasDerivAt_secondProduct L541
def SecondProductRuleEqualsCanonicalHessianTarget L627
def SecondSchlaefliAlongLineTarget L637
def MixedHingeDeficitCanonicalHessianTarget L648
theorem hingeLineDeriv_zero_eq_directional L655
theorem deficitLineDeriv_zero_eq_deficitPackage L670
def MixedHingeDeficitFromDeficitPackageTarget L687
def MixedHingeDeficitDirichletTarget L699
theorem mixedHingeDeficitFromDeficitPackage_of_dirichlet L708
def MixedHingeDeficitEdgeStencilTarget L720
theorem mixedHingeDeficitDirichlet_of_edgeStencil L729
theorem mixedHingeDeficitFromDeficitPackage_of_edgeStencil L738
theorem mixedHingeDeficitCanonicalHessian_of_deficitPackage L747
theorem mixedHingeDeficitCanonicalHessian_of_edgeStencil L765
def WeightedDeficitDerivativeStationaryTarget L778
def WeightedDeficitDerivativeEventuallyZeroTarget L793
theorem weightedDeficitDerivativeStationary_of_eventuallyZero L803
def ConformalSchlaefliAlongLineTarget L824
def LocalConformalSchlaefliAlongLineTarget L839
def ConformalSchlaefliAlongLineExpansionTarget L857
def LocalConformalSchlaefliNearZeroTarget L874
def LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget L889
def LocalConformalSchlaefliClosedFormZeroNearZeroTarget L907
theorem conformalLocalSqEdge_line_pos L917
theorem cm3_conformalTetSqEdges_line_pos_eventually L924
theorem localConformalSchlaefliClosedFormZeroNearZero L962
theorem dihedralCos3Sq_conformalTetSqEdges_line_endpoint_free_eventually L980
theorem conformalTetSqEdges_hasDerivAt_line L1025
theorem localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration L1042
theorem localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero L1115
def ConformalSchlaefliNearZeroExpansionTarget L1170
def LocalDihedralAngleLineDifferentiabilityNearZeroTarget L1188
theorem tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration L1197
theorem localDihedralAngleLineDifferentiabilityNearZero_of_flatConfiguration L1218
theorem hingeMeasureUnderConformal_eq_local_sqrt_of_incident L1233
theorem incidenceEdgeSlotPartition_edge_sum_for_tet_conformal L1279
theorem incidenceEdgeSlotPartition_sum_match_conformal L1340
theorem deficitLineDeriv_eq_neg_sum_local_nearZero L1385
theorem conformalSchlaefliNearZeroExpansion_of_angleDiff_and_partition L1508
theorem weightedDeficitDerivativeEventuallyZero_of_nearZeroExpansion_and_local L1559
theorem weightedDeficitDerivativeStationary_of_nearZeroExpansion_and_local L1579
theorem conformalSchlaefliAlongLine_of_expansion_and_local L1589

… and 62 more