OAI/Combinatorics/BalancedRyser/Incidence/AffineInjectionGuards.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.InjectionExposure.auxiliary_next_event_probability_le_budget line 11
  2. theorem OAI.Balanced.auxiliary_guarded_joining_probability_le line 33
  3. theorem OAI.Balanced.auxiliary_guarded_projection_probability_le line 52
  4. theorem OAI.Balanced.inverse_token_budget_le_two_div line 78
  5. theorem OAI.Balanced.inverse_remaining_le_two_div line 88
  6. theorem OAI.Balanced.auxiliary_guarded_joining_probability_le_two_div line 97
  7. theorem OAI.Balanced.auxiliary_guarded_projection_probability_le_two_div line 110