OAI/Combinatorics/Progressions/Probability/ContainedProgressionCubeLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_pi_sum line 15
2. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_commute line 40
3. theorem OAI.Erdos3.integerBox_cube_mean_split line 54
4. def OAI.Erdos3.containedProgressionTupleMap line 94
5. theorem OAI.Erdos3.containedProgressionTupleMap_normalized line 99
6. theorem OAI.Erdos3.containedProgressionTupleLaw_mean line 110
7. def OAI.Erdos3.containedProgressionCubeLaw line 138
8. theorem OAI.Erdos3.containedProgressionCubeLaw_complexMean line 143
9. theorem OAI.Erdos3.containedProgressionCubeLaw_sum line 162