OAI/MathematicalPhysics/CriticalSK/SmallBall.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalSK.gaussian_inverse_sqrt_bound line 72
2. lemma OAI.CriticalSK.spectralGood_sphere_smallBall line 86
3. def OAI.CriticalSK.naturalSmallBallConstant line 126
4. lemma OAI.CriticalSK.spectralGood_natural_sphere_bounds line 128
5. lemma OAI.CriticalSK.spectralGood_orientation_overlap line 188
6. instance OAI.CriticalSK.disorderLaw_probability line 219
7. lemma OAI.CriticalSK.goe_natural_spectral_bad line 223
8. lemma OAI.CriticalSK.disorder_goe_event line 238
9. lemma OAI.CriticalSK.natural_smallBallObstruction_probability line 244
10. lemma OAI.CriticalSK.naturalSmallBallConstant_pos line 271
11. lemma OAI.CriticalSK.exists_spectral_failure_parameter line 275
12. lemma OAI.CriticalSK.natural_smallBall_tight line 283