OAI/Combinatorics/Progressions/Estimates/NativeFixedFactoredQuadruples.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeCorrelationStructure.selectedMixed line 18
2. def OAI.Erdos3.NativeCorrelationStructure.selectedRank line 21
3. def OAI.Erdos3.NativeCorrelationStructure.selectedLower line 24
4. theorem OAI.Erdos3.NativeCorrelationStructure.selectedProduct_eq line 27
5. theorem OAI.Erdos3.NativeCorrelationStructure.selectedProduct_fourPoint_factorization line 30
6. theorem OAI.Erdos3.NativeCorrelationStructure.selectedCorrelator_quadruple_factored line 42
7. theorem OAI.Erdos3.NativeCorrelationStructure.exists_factored_correlation_quadruples line 61
8. theorem OAI.Erdos3.NativeCorrelationStructure.exists_fixed_factored_correlation_quadruples line 94