OAI/Combinatorics/Progressions/Probability/WeightedModeratePointMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finiteImageMass_eq_toPMF line 13
2. theorem OAI.Erdos3.integerGridMass_eq_toPMF line 24
3. theorem OAI.Erdos3.integerGridMass_eq_of_pmf_image line 30
4. theorem OAI.Erdos3.integerGridDensity_eq_of_pmf_image line 40
5. theorem OAI.Erdos3.weightedModeratePMF_zero_off_scaled_support line 63
6. theorem OAI.Erdos3.weightedModerateGridDensity_eq_pmf_on_scaled_support line 82
7. theorem OAI.Erdos3.weightedModeratePointMass_error_cutoff line 100