OAI/MathematicalPhysics/CriticalSK/OrientationBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalSK.exp_midpoint_bound line 69
2. def OAI.CriticalSK.correlatedVector line 77
3. lemma OAI.CriticalSK.correlatedVector_gram line 81
4. lemma OAI.CriticalSK.correlatedEnergy_sign line 99
5. lemma OAI.CriticalSK.correlatedMoment_sign line 109
6. lemma OAI.CriticalSK.pairMoment_correlated_lower line 118
7. lemma OAI.CriticalSK.pairMoment_min_at_orthogonal line 163
8. def OAI.CriticalSK.sphereWeightedPair line 178
9. lemma OAI.CriticalSK.sphereWeightedPair_factor line 182
10. lemma OAI.CriticalSK.sphereWeightedPair_continuous line 192
11. lemma OAI.CriticalSK.sphereWeightedPair_integral line 199
12. lemma OAI.CriticalSK.continuous_product_swap line 209
13. lemma OAI.CriticalSK.spherePair_haar_continuous line 214
14. lemma OAI.CriticalSK.pairMoment_le_partition_product line 225
15. lemma OAI.CriticalSK.sphericalVariational_deriv_integrable line 255
16. lemma OAI.CriticalSK.saddleSubcriticalError_bound line 266
17. lemma OAI.CriticalSK.sphericalVariational_supercritical_bound line 295
18. lemma OAI.CriticalSK.saddlePairDeficit_macro_bound line 339
19. lemma OAI.CriticalSK.saddlePairDeficit_macro_cubic line 349
20. lemma OAI.CriticalSK.pairMoment_abs line 368
21. lemma OAI.CriticalSK.pairMoment_variational_upper line 374
22. lemma OAI.CriticalSK.weighted_overlap_tail_term line 414
23. lemma OAI.CriticalSK.weighted_overlap_tail_sum line 440
24. lemma OAI.CriticalSK.polynomial_stretched_exponential_tendsto line 463
25. lemma OAI.CriticalSK.latticeOverlap_abs_le line 476
26. lemma OAI.CriticalSK.pairMoment_variational_upper_general line 485
27. lemma OAI.CriticalSK.sphereOverlap_density_second_moment_general line 497
28. lemma OAI.CriticalSK.saddlePairDeficit_full_cubic line 506
29. lemma OAI.CriticalSK.orientation_normalized_variance_bound line 521
30. lemma OAI.CriticalSK.orientation_normalized_overlap_bound line 579