OAI/Combinatorics/Progressions/Estimates/CommonPositivePartitionRefinement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.PositiveCyclicModel line 13
2. theorem OAI.Erdos3.PositiveCyclicNiltest.model_nonempty line 28
3. theorem OAI.Erdos3.PositiveCyclicNiltest.prod line 63
4. theorem OAI.Erdos3.real_shift_weighted_mean line 117
5. theorem OAI.Erdos3.shift_violation_weight_cap line 124
6. theorem OAI.Erdos3.exists_many_positive_cyclic_violations line 149
7. theorem OAI.Erdos3.exists_common_positive_partition line 197
8. theorem OAI.Erdos3.exists_common_positive_partition_refinement line 265