IndisputableMonolith.Geometry.ReggeActionSmoothness

declarations in this module (30)

• def GlobalZeroDeficitAtFlat L37
• structure LocalAnalyticFlatChart L43
• structure ReggeActionContDiffFromLocalChart L64
• structure FlatConfiguration L74
• def flatConfiguration_of_localChart_zeroDeficit L87
• theorem local_dihedralDenom3Poly_pos L99
• theorem local_dihedralDenom3Poly_ne_zero L106
• theorem local_dihedralDenom3_ne_zero L111
• theorem dihedralDenom3_continuousAt L117
• theorem dihedralCos3Sq_continuousAt_of_den_ne_zero L131
• theorem local_dihedralCos3Sq_continuousAt L141
• theorem conformalLocalSqEdge_contDiff L148
• theorem conformalLocalSqEdge_contDiffAt_zero L154
• theorem conformalTetSqEdges_contDiff L161
• theorem conformalTetSqEdges_zero L168
• theorem dihedralCos3Sq_conformal_continuousAt_zero L175
• theorem cmCofactor3_conformal_contDiff L193
• theorem cmCofactor3_conformal_contDiffAt_zero L200
• theorem dihedralDenom3_conformal_contDiffAt_zero L207
• theorem dihedralCos3Sq_conformal_contDiffAt_zero L232
• theorem tetDihedralAngleUnderConformal_contDiffAt_zero L246
• theorem localDeficitAngleContribution_contDiffAt_zero L267
• theorem deficitAngle_contDiffAt_zero L285
• theorem hingeMeasureUnderConformal_contDiff L307
• theorem hingeMeasureUnderConformal_contDiffAt_zero L314
• theorem reggeAction_contDiffAt_zero_of_endpoint_free L320
• theorem reggeAction_contDiffAt_zero_of_localChart L338
• def reggeActionContDiffFromLocalChart_of_localChart L345
• theorem reggeAction_contDiff_at_zero L354
• theorem deficitAngle_zero_of_flat L361