OAI/Probability/SKGap/Localization/Invert.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.invert line 10
2. lemma OAI.SKGapCutoff.invert_invert line 11
3. lemma OAI.SKGapCutoff.spin_invert line 13
4. def OAI.SKGapCutoff.invertEquiv line 16
5. lemma OAI.SKGapCutoff.sum_invert line 21
6. lemma OAI.SKGapCutoff.energy_invert line 23
7. lemma OAI.SKGapCutoff.gibbs_invert line 26
8. theorem OAI.SKGapCutoff.gibbs_spin_centered line 29
9. lemma OAI.SKGapCutoff.generator_spin line 36
10. lemma OAI.SKGapCutoff.siteVariance_pos line 40
11. lemma OAI.SKGapCutoff.siteVariance_le_one line 46
12. lemma OAI.SKGapCutoff.dirichlet_nonneg line 51
13. theorem OAI.SKGapCutoff.spin_first_second line 60
14. def OAI.SKGapCutoff.gibbsEuclideanEquiv line 82
15. lemma OAI.SKGapCutoff.gibbsEuclideanEquiv_apply line 95
16. lemma OAI.SKGapCutoff.gibbsEuclideanEquiv_symm_apply line 97
17. lemma OAI.SKGapCutoff.gibbsEuclideanEquiv_inner line 101
18. def OAI.SKGapCutoff.negativeGeneratorEuclidean line 111
19. lemma OAI.SKGapCutoff.negativeGeneratorEuclidean_lift line 116
20. lemma OAI.SKGapCutoff.negativeGeneratorEuclidean_symmetric line 121
21. lemma OAI.SKGapCutoff.negativeGeneratorEuclidean_nonneg line 133
22. def OAI.SKGapCutoff.spinEigenvalues line 143
23. def OAI.SKGapCutoff.spinEigenbasis line 148
24. def OAI.SKGapCutoff.spinSpectralCoefficient line 153
25. def OAI.SKGapCutoff.spinSpectralMass line 158
26. def OAI.SKGapCutoff.spinSpectralMeasure line 163