OAI/Probability/SKGap/Terminal/SpinCovarianceMeasure.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.polynomial_approximation_semicircle_support line 176
2. lemma OAI.SKGapCutoff.semicircle_support_measure_ext line 192
3. def OAI.SKGapCutoff.spinCovarianceMeasure line 226
4. lemma OAI.SKGapCutoff.spinCovarianceMeasure_ae_mem line 229
5. lemma OAI.SKGapCutoff.spinCovarianceMeasure_integral line 233
6. lemma OAI.SKGapCutoff.spinCovarianceMeasure_probability line 244
7. theorem OAI.SKGapCutoff.spinCovarianceMeasure_eq_of_moments line 259
8. def OAI.SKGapCutoff.Regression.spinEnergyAverage line 277
9. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_gaussian line 280
10. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_mean line 286
11. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_variance line 295
12. lemma OAI.SKGapCutoff.Regression.hasSubgaussianMGF_mono_parameter line 325
13. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_centered_subgaussian line 332
14. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_planted_tail line 355
15. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_planted_exponential line 372
16. lemma OAI.SKGapCutoff.Regression.continuous_spinEnergyAverage line 410
17. theorem OAI.SKGapCutoff.Regression.quenched_spinEnergyAverage_exponential line 415
18. lemma OAI.SKGapCutoff.Regression.spinEnergyAverage_abs_le_opNorm line 426