OAI/Combinatorics/BalancedRyser/Deletion/DeletionDomination2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.DeletionLaw.atom_le_of_cylinder line 10
  2. theorem OAI.Balanced.DeletionLaw.six_mul_choose_three_le line 30
  3. theorem OAI.Balanced.DeletionLaw.assignment_normalization_le line 36
  4. theorem OAI.Balanced.DeletionLaw.assignment_factorization line 45
  5. theorem OAI.Balanced.DeletionLaw.assignment_bound_le_uniform line 52
  6. theorem OAI.Balanced.DeletionLaw.conditioned_bound_of_joint line 65
  7. theorem OAI.Balanced.DeletionLaw.six_mul_choose_three_eq line 86
  8. theorem OAI.Balanced.DeletionLaw.assignment_ratio_exact line 96
  9. theorem OAI.Balanced.DeletionLaw.conditioned_ratio_of_assignment_bound line 107
  10. theorem OAI.Balanced.DeletionLaw.deletionMass_le_assignment_bound line 136
  11. theorem OAI.Balanced.DeletionLaw.finite_domination line 147
  12. theorem OAI.Balanced.DeletionLaw.exponential_domination line 153