OAI/Combinatorics/BalancedRyser/Deletion/DeletionLawNormalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.DeletionLaw.offsetAverage_nonneg line 12
  2. theorem OAI.Balanced.DeletionLaw.offsetAverage_le_of_atom_bound line 16
  3. theorem OAI.Balanced.DeletionLaw.successMass_nonneg line 22
  4. theorem OAI.Balanced.DeletionLaw.successMass_le_one line 26
  5. theorem OAI.Balanced.DeletionLaw.deletionMass_nonneg line 33
  6. theorem OAI.Balanced.DeletionLaw.deletionMass_le_successMass line 43
  7. theorem OAI.Balanced.DeletionLaw.sum_deletionMass line 53
  8. theorem OAI.Balanced.DeletionLaw.deletionMass_eq_zero_of_invalid line 66
  9. theorem OAI.Balanced.DeletionLaw.conditionedDeletionMass_nonneg line 85
  10. theorem OAI.Balanced.DeletionLaw.sum_conditionedDeletionMass line 90
  11. theorem OAI.Balanced.DeletionLaw.conditionedDeletionMass_eq_zero_of_invalid line 95