OAI/Probability/SKGap/Localization/UpperCoefficient.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.upperCoefficient line 16
2. lemma OAI.SKGapCutoff.energy_sampled line 19
3. lemma OAI.SKGapCutoff.integral_exp_gaussian_linear line 40
4. lemma OAI.SKGapCutoff.integrable_exp_gaussian_linear line 55
5. lemma OAI.SKGapCutoff.sum_upperCoefficient_sq line 62
6. def OAI.SKGapCutoff.replicaOverlap line 81
7. lemma OAI.SKGapCutoff.sum_upperCoefficient_mul line 84
8. lemma OAI.SKGapCutoff.integrable_exp_energy_sampled line 108
9. lemma OAI.SKGapCutoff.integral_exp_energy_sampled line 113
10. lemma OAI.SKGapCutoff.integrable_partition_sampled line 125
11. lemma OAI.SKGapCutoff.integral_partition_sampled line 129
12. lemma OAI.SKGapCutoff.sum_upperCoefficient_add_sq line 137
13. lemma OAI.SKGapCutoff.combined_energy_sampled line 146
14. lemma OAI.SKGapCutoff.integrable_exp_combined_energy line 151
15. lemma OAI.SKGapCutoff.integral_exp_combined_energy line 157
16. lemma OAI.SKGapCutoff.partition_sq_eq_sum line 170
17. lemma OAI.SKGapCutoff.integrable_partition_sq_sampled line 175
18. lemma OAI.SKGapCutoff.integral_partition_sq_sampled line 181
19. def OAI.SKGapCutoff.multiplySpin line 191
20. lemma OAI.SKGapCutoff.spin_multiplySpin line 193
21. lemma OAI.SKGapCutoff.multiplySpin_self line 197
22. def OAI.SKGapCutoff.multiplySpinEquiv line 202
23. lemma OAI.SKGapCutoff.replicaOverlap_eq_magnetization line 208
24. lemma OAI.SKGapCutoff.sum_replicaOverlap line 212
25. lemma OAI.SKGapCutoff.partition_second_moment_identity line 217
26. lemma OAI.SKGapCutoff.integral_exp_gaussian_quadratic line 234
27. lemma OAI.SKGapCutoff.integrable_exp_gaussian_quadratic line 252
28. lemma OAI.SKGapCutoff.sign_sum_exponential line 259
29. lemma OAI.SKGapCutoff.gaussian_sign_square_identity line 273
30. lemma OAI.SKGapCutoff.cosh_scaled_pow_le line 284
31. lemma OAI.SKGapCutoff.sign_square_moment_le line 296
32. lemma OAI.SKGapCutoff.partition_second_moment_bound line 320