OAI/Probability/SKGap/Localization/SemicircleDensity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.semicircleDensity line 170
2. def OAI.SKGapCutoff.semicircleMeasure line 172
3. lemma OAI.SKGapCutoff.semicircleDensity_continuous line 175
4. lemma OAI.SKGapCutoff.semicircleDensity_pos line 178
5. instance OAI.SKGapCutoff.semicircleMeasure_locallyFinite line 184
6. lemma OAI.SKGapCutoff.semicircleMeasure_right_neighborhood line 187
7. lemma OAI.SKGapCutoff.semicircleDensity_eq_zero_outside line 206
8. lemma OAI.SKGapCutoff.semicircleDensity_integrable line 213
9. lemma OAI.SKGapCutoff.integral_semicircleDensity line 220
10. instance OAI.SKGapCutoff.semicircleMeasure_probability line 238
11. def OAI.SKGapCutoff.spinEdgeWeight line 246
12. lemma OAI.SKGapCutoff.spinEdgeWeight_eq_squared line 247
13. lemma OAI.SKGapCutoff.spinCovariance_denominator_pos line 251
14. lemma OAI.SKGapCutoff.spin_edge_localization line 256
15. theorem OAI.SKGapCutoff.spin_edge_bound_from_polynomial_tests line 283
16. lemma OAI.SKGapCutoff.le_one_of_polynomial_power_bound line 308
17. lemma OAI.SKGapCutoff.strict_renewal_bound line 322
18. lemma OAI.SKGapCutoff.second_renewal_bound line 330