IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence

declarations in this module (15)

• theorem periodicDispSqEdge_pos L90
• def planeWaveTetVelocity L96
• theorem planeWaveTetSqEdges_apply L105
• theorem planeWaveTetSqEdges_zero L116
• theorem planeWaveTetSqEdges_contDiff L125
• theorem planeWaveEdgeValue_contDiff L139
• theorem tetDihedralAngle_planeWave_contDiffAt L159
• theorem edgeAngleContribution_planeWave_contDiffAt L185
• theorem deficit_planeWave_contDiffAt L201
• theorem sqrtEdge_planeWave_contDiffAt L213
• theorem planeWaveActionProfile_contDiffAt L223
• theorem slope_average_eq L241
• theorem tendsto_centeredSecondDifference_of_contDiffAt L262
• theorem planeWave_TTBlochSymbolIs_secondVariation L388
• theorem planeWave_TTBlochSymbol_exists L407