OAI/Probability/SphericalField/Positivity/ReplicaMean.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.replicaMean line 16
2. lemma OAI.SphericalPerceptron.inner_replicaMean line 18
3. lemma OAI.SphericalPerceptron.replicaMean_norm_sq_le line 26
4. lemma OAI.SphericalPerceptron.inner_replicaMean_eq line 54
5. lemma OAI.SphericalPerceptron.duplicate_blocks_bound line 63
6. lemma OAI.SphericalPerceptron.arbitrary_duplicate_blocks_equal line 103
7. lemma OAI.SphericalPerceptron.replicaMean_norm_le_one line 120
8. lemma OAI.SphericalPerceptron.inner_replicaMean_le line 135
9. lemma OAI.SphericalPerceptron.le_inner_replicaMean line 147
10. lemma OAI.SphericalPerceptron.duplicate_ordered_blocks_bound line 159
11. lemma OAI.SphericalPerceptron.posSemidef_standard_basis_inner line 194
12. def OAI.SphericalPerceptron.triangleConstraints line 202
13. lemma OAI.SphericalPerceptron.triangleConstraints_measurable line 208
14. lemma OAI.SphericalPerceptron.triangleConstraints_diag line 213
15. lemma OAI.SphericalPerceptron.triangleConstraints_cut line 216
16. def OAI.SphericalPerceptron.tripleIndex line 225
17. lemma OAI.SphericalPerceptron.tripleLabels_tripleIndex line 228
18. lemma OAI.SphericalPerceptron.tripleIndex_ne line 233
19. lemma OAI.SphericalPerceptron.tripleIndex_inj line 239
20. lemma OAI.SphericalPerceptron.triangle_pattern_psd_bound line 248
21. theorem OAI.SphericalPerceptron.gg_triangle_pattern_bound line 284