OAI/Probability/SKGap/Terminal/GibbsExpectationMono.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.gibbsExpectation_mono line 10
2. lemma OAI.SKGapCutoff.spin_variance line 14
3. theorem OAI.SKGapCutoff.finite_gap_le_one line 20
4. lemma OAI.SKGapCutoff.spectral_bilinear_dirichlet line 32
5. lemma OAI.SKGapCutoff.spectral_gradient_correlation line 45
6. theorem OAI.SKGapCutoff.exact_gradient_semigroup_positive line 62
7. lemma OAI.SKGapCutoff.exact_gradient_semigroup_symmetric line 73
8. theorem OAI.SKGapCutoff.exact_gradient_semigroup_gap line 83