module module

`IndisputableMonolith.Geometry.ReggeActionFirstVariation`

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

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

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import
IndisputableMonolith.Geometry.ReggeActionSecondVariation module_import
IndisputableMonolith.Gravity.TensorShearSector module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.ReggeActionSmoothness module_import
IndisputableMonolith.Geometry.SchlaefliTetrahedronProof module_import
IndisputableMonolith.Geometry.SchlaefliTriangulation3D module_import

declarations in this module (65)

def linePotential L33
theorem linePotential_zero L37
theorem continuousLinearMap_apply_eq_sum_single L45
theorem functionUpdate_hasDerivAt_single L68
def conformalLocalSqEdgeDirectionalDeriv L85
theorem conformalLocalSqEdge_hasDerivAt_line_zero L91
theorem conformalTetSqEdges_hasDerivAt_line_zero L121
theorem dihedralDenom3_contDiffAt_nonDegenerate L130
theorem dihedralCos3Sq_contDiffAt_nonDegenerate L160
theorem dihedralAngle3Sq_contDiffAt_nonDegenerate L177
theorem fderiv_dihedralAngle3Sq_apply_single L190
def hingeMeasureDirectionalDeriv L247
theorem hingeMeasureUnderConformal_hasDerivAt_line_zero L253
theorem linePotential_hasDerivAt_zero L277
theorem reggeAction_along_line_hasDerivAt_fderiv L285
def ReggeActionCriticalAtZero L308
def ReggeActionDirectionalCriticalAtZero L314
theorem reggeActionCriticalAtZero_of_directional L319
structure ReggeActionFirstVariationFormula L330
structure ReggeActionDirectionalFirstVariationFormula L342
structure LocalDihedralDirectionalDerivativePackage L354
def localDihedralDirectionalDerivativePackage_of_flat L363
def localEdgeLengthDirectionalDeriv L403
def localAngleLengthChainDeriv L412
def localAngleSqEdgeChainDeriv L420
theorem localAngleLengthChainDeriv_eq_sqEdgeChainDeriv L427
theorem local_conformal_schlaefli_cancellation L459
structure LocalAngleLengthChainRulePackage L494
structure LocalAngleSqEdgeChainRulePackage L504
def localAngleSqEdgeChainRulePackage_of_flat L512
def localAngleLengthChainRulePackage_of_sqEdge L567
def localDihedralDirectionalDerivativePackage_of_lengthChain L577
def deficitDirectionalDerivFromLocalAngles L584
structure DeficitAngleDirectionalDerivativePackage L594
theorem localDeficitAngleContribution_hasDerivAt_from_localAngles L606
theorem deficitAngle_hasDerivAt_from_localAngles L621
def deficitPackage_of_localAngles L654
def ConformalSchlaefliCancellation L669
def ConformalSchlaefliIncidenceBookkeeping L679
structure IncidenceEdgeSlotBookkeeping L697
structure IncidenceEdgeSlotPartition L714
def incidenceEdgeSlotBookkeeping_of_partition L794
theorem conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping L831
theorem conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping L862
def deficitPackage_of_conformalSchlaefliCancellation L881
theorem directionalFirstVariationFormula_of_deficitPackage L888
theorem firstVariationFormula_of_directionalFormula L950
theorem directionalCritical_of_firstVariationFormula_of_zeroDeficit L961
theorem reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit L973
structure ReggeActionFirstVariationInput L985
def reggeActionFirstVariationInput_of_directional L990
def reggeActionFirstVariationInput_of_firstVariationFormula L997
def reggeActionFirstVariationInput_of_localAngles L1006
def reggeActionFirstVariationInput_of_conformalSchlaefliCancellation L1017
def reggeActionFirstVariationInput_of_incidenceBookkeeping L1026
def reggeActionFirstVariationInput_of_edgeSlotBookkeeping L1043
def reggeActionFirstVariationInput_of_edgeSlotPartition L1055
theorem reggeAction_firstVariation_zero L1065
structure ReggeActionRemainderFirstVariationInput L1076
theorem reggeActionRemainder_fderiv_zero L1082
theorem hasFDerivAt_finset_sum_zero L1089
theorem hessianQuadratic_term_hasFDerivAt_zero L1110
theorem hessianQuadratic_hasFDerivAt_zero L1134
theorem half_hessianQuadratic_hasFDerivAt_zero L1149
def reggeActionRemainderFirstVariationInput_of_firstVariation L1160