OAI/Combinatorics/Progressions/Sampling/FiniteSamplingMoment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos3.CyclicMZ.step_one line 21
2. lemma OAI.Erdos3.CyclicMZ.step_one' line 47
3. lemma OAI.Erdos3.CyclicMZ.step_two_aux line 59
4. lemma OAI.Erdos3.CyclicMZ.step_two line 86
5. lemma OAI.Erdos3.CyclicMZ.step_three line 101
6. lemma OAI.Erdos3.CyclicMZ.step_four line 115
7. lemma OAI.Erdos3.CyclicMZ.step_six line 125
8. lemma OAI.Erdos3.CyclicMZ.step_seven line 139
9. lemma OAI.Erdos3.CyclicMZ.step_eight line 146
10. lemma OAI.Erdos3.CyclicMZ.end_step line 154
11. theorem OAI.Erdos3.CyclicMZ.Real.marcinkiewicz_zygmund' line 182
12. theorem OAI.Erdos3.CyclicMZ.Real.marcinkiewicz_zygmund line 220
13. theorem OAI.Erdos3.CyclicMZ.RCLike.marcinkiewicz_zygmund line 252