OAI/Combinatorics/BalancedRyser/Candidates/FreshExternalCountBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.FreshExternalWitness.sourceEvent line 15
  2. theorem OAI.Balanced.FreshExternalWitness.sourceEvent_iff_witnessEvent line 24
  3. theorem OAI.Balanced.FreshExternalWitness.sourceEvent_eligible line 40
  4. theorem OAI.Balanced.FreshExternalWitness.sourceEvent_freshPairs_iff line 46
  5. theorem OAI.Balanced.FreshExternalWitness.sourceEvent_has_orientedEvent line 66
  6. theorem OAI.Balanced.FreshExternalWitness.outerProbability_mono line 82
  7. theorem OAI.Balanced.FreshExternalWitness.sourceEvent_probability_le line 90
  8. def OAI.Balanced.FreshExternalWitness.sourceProbabilitySum line 109
  9. theorem OAI.Balanced.FreshExternalWitness.sourceProbabilitySum_le line 115
  10. def OAI.Balanced.FreshExternalWitness.sourceWitnessCount line 130
  11. theorem OAI.Balanced.FreshExternalWitness.sum_roots_eq_all line 136
  12. theorem OAI.Balanced.FreshExternalWitness.sourceLabelCount_eq line 152
  13. theorem OAI.Balanced.FreshExternalWitness.canonical_fresh_count_eq line 167
  14. theorem OAI.Balanced.FreshExternalWitness.integral_sourceWitnessCount line 197
  15. theorem OAI.Balanced.FreshExternalWitness.sourceWitnessCount_mean_le line 215
  16. theorem OAI.Balanced.FreshExternalWitness.canonical_fresh_count_integral_le line 222