IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation

declarations in this module (37)

• def edgeCoeff L110
• def edgeSqrtDeriv L116
• theorem hasDerivAt_edgeValue L122
• theorem hasDerivAt_sqrtEdge L137
• theorem hasDerivAt_angle_directional L161
• def slotAngleDeriv L206
• theorem hasDerivAt_slotAngle L217
• def contribDeriv L263
• theorem hasDerivAt_contrib L270
• def deficitDeriv L291
• def PathGoodAt L297
• theorem pathGoodAt_zero L311
• theorem eventually_pathGoodAt L329
• theorem hasDerivAt_deficit L369
• def firstVariationIntegrand L392
• theorem hasDerivAt_planeWaveActionProfile L402
• theorem slotMatch_mul L430
• theorem sum_edges_slotMatch L441
• theorem sum_sqrt_slotAngleDeriv_eq_zero L504
• theorem sum_sqrt_deficitDeriv_eq_zero L544
• theorem deficit_planeWave_zero L602
• theorem firstVariationIntegrand_zero L611
• theorem trueReggeAction_firstVariation_flat_eq_zero L632
• def flatSlotSqrtDeriv L642
• def flatSlotAngleDeriv L648
• theorem edgeSqrtDeriv_localEdge_zero L655
• theorem slotAngleDeriv_zero L666
• theorem sum_edgeSqrtDeriv_deficitDeriv_flat L675
• def reducedFirstVariation L733
• theorem firstVariationIntegrand_eq_reduced L741
• theorem deriv_actionProfile_eventuallyEq_reduced L750
• theorem edgeSqrtDeriv_differentiableAt L761
• theorem hasDerivAt_reducedFirstVariation_flat L780
• theorem trueReggeAction_secondVariation_flat_schlaefli L825
• def axisReducedSecondVariation L846
• theorem axisReducedSecondVariation_applies L856
• theorem planeWave_TTBlochSymbolIs_reduced L870