IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D

declarations in this module (37)

• abbrev Pt L70
• def phase L75
• def pd L78
• def frobSq L84
• theorem phase_update L86
• theorem hasDerivAt_phase_update L104
• theorem phase_update_self L114
• theorem pd_cos L120
• theorem pd_sin L133
• def hWave L147
• def linChristoffel L154
• def chrAmp L159
• theorem linChristoffel_eq L162
• def linRicci L172
• def ricciAmp L177
• theorem linRicci_eq L180
• theorem sum_k_mul_row L205
• theorem sum_k_chrAmp L214
• theorem sum_chrAmp_trace L229
• theorem ricciAmp_tt L242
• theorem linRicci_tt L251
• def linRicciScalar L258
• def linEinstein L262
• theorem linRicciScalar_tt L266
• theorem linEinstein_tt L279
• def ehSecondVariationDensity L290
• theorem ehSecondVariationDensity_tt L293
• def phaseAverage L313
• theorem phaseAverage_const_mul L316
• theorem phaseAverage_cos_sq L325
• def densityOfPhase L335
• theorem density_factors_through_phase L338
• def ehFace L344
• theorem ehFace_eq_phaseAverage L349
• theorem ehFace_eq_average_of_density L355
• theorem ehFace_rigid L367
• def provenance L389