module module

`IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4D`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D module_import

declarations in this module (15)

theorem phaseAverage_const L82
theorem phaseAverage_sin_sq L89
theorem phaseAverage_sin_sq_affine L99
def exactDensityTT L126
def exactDensityTrace L130
def exactDensityLongitudinal L134
theorem exactDensityTT_average L136
theorem exactDensityTrace_average L144
theorem exactDensityLongitudinal_average L151
theorem exact_average_eq_ehFace L167
theorem a3_agrees_with_exact L177
theorem trace_decoy_misses_the_face L191
theorem longitudinal_decoy_misses_the_face L205
theorem exact_density_rigid L217
def provenance L228