OAI/Combinatorics/Progressions/Estimates/NativeGlobalErrorSplitting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeTwoVariableSplit.exists_fixed_correlating_term line 16
2. theorem OAI.Erdos3.NativeVectorEquivalence.transfer_correlation line 66
3. theorem OAI.Erdos3.NativeNilsequenceExpansion.absorb_correlation line 133
4. def OAI.Erdos3.NativeCorrelationStructure.normalizedErrorCorrelator line 171
5. theorem OAI.Erdos3.NativeCorrelationStructure.normalizedErrorCorrelator_norm line 175
6. theorem OAI.Erdos3.NativeCorrelationStructure.normalizedErrorCorrelator_correlation line 184
7. def OAI.Erdos3.GlobalErrorSplittingStatement line 236
8. theorem OAI.Erdos3.NativeCorrelationStructure.absorb_split_term line 274
9. theorem OAI.Erdos3.exists_split_global_error line 326