module module

`IndisputableMonolith.Gravity.SevenGaps.DiscreteLichnerowicz`

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 (2)

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

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination module_import

declarations in this module (50)

def discLap L88
def fourierMode L93
theorem fourierMode_periodic L98
lemma fourierMode_step L114
lemma fourierMode_step_down L125
lemma exp_add_exp_neg_mul_I L136
theorem discLap_fourierMode_apply L147
theorem discLap_fourierMode L190
def discreteEigenvalue L201
theorem discreteEigenvalue_tendsto L219
theorem discrete_eigenvalue_tendsto_raw L274
abbrev Site3 L283
abbrev LatticeTensorField L286
def unitVec L289
lemma fst_add_e0 L294
lemma fst_sub_e0 L295
lemma fst_add_e1 L296
lemma fst_sub_e1 L297
lemma fst_add_e2 L298
lemma fst_sub_e2 L299
def discDiv L303
def discLap3 L307
def planeH L314
lemma planeH_apply L318
theorem planeH_periodic_axis L325
theorem planeH_shift_yz L333
theorem planeH_transverse L343
theorem discLap3_planeH L353
def epsPlus L369
def epsCross L372
theorem epsPlus_isSymm L374
theorem epsCross_isSymm L378
theorem epsPlus_traceless L382
theorem epsCross_traceless L387
theorem epsPlus_row0 L392
theorem epsCross_row0 L396
theorem epsPlus_col0 L400
theorem epsCross_col0 L404
theorem polarizations_linearIndependent L410
def continuumProfile L432
def continuumPlaneH L436
theorem continuumProfile_hasDerivAt L441
theorem continuumProfile_second_deriv L457
def lichnerowiczFlatEigenvalue L484
theorem discrete_tt_spectrum_converges_to_flat_lichnerowicz L514
structure OperatorConvergenceStatus L535
def status L557
theorem status_flat_tt_convergence_proved L562
theorem status_curved_background_open L565
theorem status_qnm_spectrum_open L568