IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight

declarations in this module (34)

• def stencilWeight L83
• theorem stencilWeight_eq_sqrt_globalSqEdge L88
• theorem stencilWeight_values L96
• theorem stencilWeight_nonneg L103
• def shiftVertex L109
• theorem periodicEdge_endpoints_eq L112
• def freudenthalStencilEnergy L118
• def toPotential L123
• theorem toPotential_symm_apply L127
• theorem canonical_globalSqEdge_eq L134
• theorem canonical_edgeVerts_eq L139
• theorem canonicalPeriodic_noSelfLoopEdges L147
• def periodicEdgeProdEquiv L155
• theorem canonicalEdgeStencil_eq_freudenthalStencil L163
• theorem hessianQuadratic_canonical_eq_freudenthalStencil L204
• def stencilNormalization L229
• def meshSize L233
• theorem freudenthal_stencil_identity L245
• def scaledCanonicalEnergy L264
• theorem scaledCanonicalEnergy_eq_scaled_stencil L271
• def dispReal L283
• theorem dispReal_matches_dispBits L294
• def stencilMomentTensor L303
• theorem stencilMomentTensor_eq L311
• theorem stencilMomentTensor_symm L319
• theorem stencilMomentTensor_quadratic_eq L327
• theorem stencilMomentTensor_psd L336
• theorem sqrt_two_add_sqrt_three_pos L342
• theorem stencilMomentTensor_diag_pos L349
• theorem stencilMomentTensor_ne_zero L357
• theorem stencilMomentTensor_offDiag_pos L361
• theorem stencilMomentTensor_not_isotropic L370
• structure StencilPreflightStatus L392
• def stencilPreflightStatus L407