OAI/Probability/SKGap/Terminal/SpinSpectralMassBelow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.spinSpectralMassBelow line 15
2. lemma OAI.SKGapCutoff.spinSpectralMassBelow_nonneg line 19
3. lemma OAI.SKGapCutoff.spinSpectralMeasure_Iic line 28
4. lemma OAI.SKGapCutoff.spinCorrelation_eq_spectralSum line 46
5. lemma OAI.SKGapCutoff.spinCorrelation_lower_of_mass line 54
6. theorem OAI.SKGapCutoff.worstContinuous_lower_from_spectralMass line 67