OAI/Combinatorics/Progressions/Probability/TranslatedWeightedCubeLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.normalizedScalarCubeSourceOfWeight_mean line 11
2. theorem OAI.Erdos3.normalizedScalarCubeSourceOfWeight_primitive line 30
3. theorem OAI.Erdos3.shiftScalarCube_neg_shift line 52
4. def OAI.Erdos3.translatedCubeWeight line 57
5. theorem OAI.Erdos3.scalarCubeResidueWeights_translated_mean line 60
6. theorem OAI.Erdos3.normalizedWeightedCube_translated_mean line 70