IndisputableMonolith.Relativity.Geometry.LocalEquilibriumAreaVariation

declarations in this module (14)

• structure LocalAreaCongruenceData L38
• theorem deriv_area_eq_expansion_mul_area L48
• theorem hasDerivAt_areaRate_zero L56
• theorem hasDerivAt_areaRate_eq_neg_area_mul_ricciNull L66
• theorem hasDerivAt_deriv_area_eq_neg_area_mul_ricciNull L85
• theorem deriv_deriv_area_zero_eq_neg_area_mul_ricciNull L95
• theorem iteratedDeriv_two_area_zero_eq_neg_area_mul_ricciNull L104
• def areaRateSlope L115
• theorem areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_expansion L124
• theorem areaRateSlope_ne_neg_area_mul_ricciNull_of_nonzero_shear L146
• theorem decoy_nonzero_expansion_areaRate_ne L163
• theorem decoy_nonzero_shear_areaRate_ne L168
• def scaledAreaRateSlope L176
• theorem decoy_areaLaw_coefficient_two_changes_equilibrium L186