OAI/Combinatorics/BalancedRyser/Local/LocalInjectionLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.UsedEventUnion.uniform_bind_probability_eq_mean line 12
  2. theorem OAI.Balanced.Local.UsedEventUnion.nonempty_tokenInjections_of_budget line 33
  3. theorem OAI.Balanced.Local.UsedEventUnion.nonempty_tokenInjections_of_ten_budget line 41
  4. def OAI.Balanced.Local.UsedEventUnion.injectionAlignedLaw line 45
  5. theorem OAI.Balanced.Local.UsedEventUnion.mem_support_injectionAlignedLaw line 53
  6. theorem OAI.Balanced.Local.UsedEventUnion.injectionAverage_eq_injectionAlignedLaw line 72
  7. theorem OAI.Balanced.Local.UsedEventUnion.injectionAverage_le_joint_probability line 88
  8. theorem OAI.Balanced.Local.UsedEventUnion.injectionAverage_le_one line 105