OAI/Combinatorics/Progressions/Estimates/IndependentFiniteConditioning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.ext_weight line 11
2. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_inter_pos_of_condition line 18
3. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_condition line 24
4. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_condition_condition_mean line 40
5. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_mem line 57
6. def OAI.Erdos3.FiniteProbabilityWeights.piRestrictionSet line 66
7. theorem OAI.Erdos3.FiniteProbabilityWeights.mem_piRestrictionSet line 69
8. theorem OAI.Erdos3.FiniteProbabilityWeights.piRestriction_mass line 73
9. theorem OAI.Erdos3.FiniteProbabilityWeights.piRestriction_mass_pos line 84
10. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_condition line 90