OAI/Combinatorics/Progressions/Probability/FiniteExcessMassCap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.FiniteProbabilityWeights.excessMass line 12
2. theorem OAI.Erdos3.FiniteProbabilityWeights.excessMass_nonneg line 16
3. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_le_of_excessMass line 20
4. theorem OAI.Erdos3.FiniteProbabilityWeights.excessMass_le_of_mass_le line 33
5. theorem OAI.Erdos3.FiniteProbabilityWeights.excessMass_antitone_cap line 59
6. theorem OAI.Erdos3.FiniteProbabilityWeights.excessMass_max_one_le line 68
7. theorem OAI.Erdos3.marginalCap_max_one_exp_bound line 77