OAI/Combinatorics/EuclideanRamsey/GramCompletion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanRamsey.trace_gram_complement line 27
2. lemma OAI.EuclideanRamsey.exists_gram_sqrt line 48
3. lemma OAI.EuclideanRamsey.gram_fromCols line 57
4. theorem OAI.EuclideanRamsey.complete_gram_pair line 63
5. lemma OAI.EuclideanRamsey.row_gram_distance line 101
6. theorem OAI.EuclideanRamsey.two_scale_of_signed_rows line 123
7. lemma OAI.EuclideanRamsey.evaluation_coset_pushforward line 183
8. lemma OAI.EuclideanRamsey.lattice_affine_evaluation line 194
9. lemma OAI.EuclideanRamsey.scaled_second_moment line 215
10. theorem OAI.EuclideanRamsey.realCriterion_two_scale line 251