OAI/Combinatorics/Progressions/Estimates/UnconditionedSmoothSlopeCap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.selectedResidueSmoothWeight_one line 10
2. theorem OAI.Erdos3.selectedResidueSmoothMass_one line 18
3. theorem OAI.Erdos3.selectedResidueSmoothPMF_one line 24
4. theorem OAI.Erdos3.independentProductPMF_slopes line 34
5. theorem OAI.Erdos3.shiftedSmoothProductPMF_slopes_cap line 53
6. theorem OAI.Erdos3.selectedResidueFiniteLaw_one_slopes_cap line 66