OAI/MathematicalPhysics/CriticalSK/RelaxationBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalSK.kernel_energy_pair_identity line 13
2. lemma OAI.CriticalSK.variance_pair_identity line 37
3. lemma OAI.CriticalSK.kernel_energy_minorization line 54
4. lemma OAI.CriticalSK.exists_finite_poincare line 71
5. lemma OAI.CriticalSK.variance_nonneg_full line 97
6. lemma OAI.CriticalSK.dirichlet_le_sites_variance line 100
7. lemma OAI.CriticalSK.variance_linear_pos_full line 109
8. lemma OAI.CriticalSK.full_ratios_bdd line 117
9. lemma OAI.CriticalSK.linearRayleigh_le_relaxationTime line 130
10. theorem OAI.CriticalSK.critical_relaxation_lower_bound line 138