OAI/Combinatorics/Progressions/Probability/FiniteConditionedMass.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteProbabilityWeights.uniform line 12
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_mean line 19
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_complexMean line 24
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_correlation line 30
  5. def OAI.Erdos3.FiniteProbabilityWeights.eventProbability line 44
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_nonneg line 49
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_false line 54
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_mono line 60
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_union_bound line 70
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_pi_product line 88
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_pi line 98
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_mass line 126
  13. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_condition_weight_le line 130
  14. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_condition_mean line 142
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_eventProbability_le line 164
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.eventProbability_le_of_weight_le line 175
  17. theorem OAI.Erdos3.disjoint_cells_card_mul_le line 197
  18. theorem OAI.Erdos3.finite_cell_event_probability_le line 209
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_mass line 242
  20. theorem OAI.Erdos3.FiniteProbabilityWeights.mass_inter_le_condition_mass line 252
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_weight_le line 259