IndisputableMonolith.Geometry.ReggeActionConcrete

declarations in this module (45)

• def conformalLocalSqEdge L29
• def conformalTetSqEdges L37
• def tetDihedralAngleUnderConformal L45
• def localDeficitAngleContribution L51
• def deficitAngle L59
• def hingeMeasureUnderConformal L65
• def reggeAction L73
• def reggeActionSecondOrder L83
• def reggeActionRemainder L91
• theorem hessianQuadratic_zeroPotential L98
• theorem reggeAction_taylor_decomposition L106
• theorem reggeActionRemainder_zero L119
• theorem reggeActionSecondOrder_secondVariation L128
• def canonicalEdgePairWeight L142
• def canonicalDualWeight L152
• theorem canonicalEdgePairWeight_symm L157
• theorem canonicalDualWeight_symm L177
• theorem canonicalDualWeight_nonneg L184
• def canonicalReggeHessian L198
• theorem canonicalReggeHessian_symm L204
• theorem canonicalReggeHessian_row_sum_zero L215
• theorem canonicalReggeHessian_offDiag_eq_neg_weight L235
• def canonicalDirichletEnergy L245
• theorem canonicalDirichletEnergy_nonneg L251
• theorem canonicalReggeHessian_quadratic_expanded L263
• theorem canonicalDirichletEnergy_expanded L285
• theorem canonicalReggeHessian_quadratic_eq_dirichlet L384
• theorem canonicalReggeHessian_quadratic_nonneg L392
• def canonicalEdgeStencilDirichletEnergy L401
• def CanonicalDirichletEqualsEdgeStencilTarget L408
• def CanonicalEdgePairWeightReindexTarget L417
• def NoSelfLoopEdges L425
• theorem canonicalEdgePairWeightReindex_of_noSelfLoop L428
• def CanonicalEdgeStencilSumCommTarget L527
• theorem canonicalEdgeStencilSumComm L536
• theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex L561
• theorem canonicalEdgeStencilDirichletEnergy_nonneg L583
• structure ConcreteReggeSecondOrderData L595
• def canonicalReggeSecondOrderData L607
• structure ConcreteReggeActionData L619
• def GenuineReggeHessianTarget L630
• theorem genuineReggeHessianTarget L636
• def reggeHessianData_of_concrete L641
• def reggeHessianData_of_secondOrder L654
• theorem genuine_regge_hessian_of_concrete L665