module module

`IndisputableMonolith.Gravity.Analysis.OneModeCylinderPreflight`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.SpectralConvergence module_import

declarations in this module (21)

def latticeEigenvalue L104
def continuumEigenvalue L109
def modeVarianceReal L113
def modeVariance L116
def modeMeasure L120
theorem latticeEigenvalue_nonneg L123
theorem modeVarianceReal_nonneg L128
theorem coe_modeVariance L133
instance instIsProbabilityMeasureModeMeasure L139
theorem integral_exp_modeMeasure L150
theorem charFun_modeMeasure L161
theorem secondMoment_modeMeasure L172
theorem latticeEigenvalue_lower_bound L187
theorem latticeEigenvalue_pos L212
theorem modeVarianceReal_pos L225
theorem modeVariance_ne_zero L232
theorem modeVarianceReal_rate L243
theorem modeVarianceReal_tendsto L292
theorem secondMoment_tendsto L300
theorem charFun_modeMeasure_tendsto L312
theorem limitVariance_pos L334