OAI/Combinatorics/Progressions/Lattices/SelectedResidueCutoffDomination.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.selectedResidueSmoothWeight_normalized_norm_le line 15
2. theorem OAI.Erdos3.selectedResidueSmoothPMF_normalized_norm_le_of_pos line 22
3. theorem OAI.Erdos3.selectedResidueFiniteLaw_normalized_norm_le line 31
4. theorem OAI.Erdos3.selectedJointFiniteLaw_normalized_norm_le line 43
5. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mono_positive_support line 68
6. theorem OAI.Erdos3.selectedResidueFiniteLaw_event_eq_map_true line 85
7. theorem OAI.Erdos3.selectedResidueFiniteLaw_cutoff_le_event line 102