OAI/Combinatorics/BalancedRyser/Deletion/DeletionDomination.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.DeletionLaw.Offset line 9
  2. abbrev OAI.Balanced.DeletionLaw.Split line 10
  3. abbrev OAI.Balanced.DeletionLaw.Weight line 11
  4. abbrev OAI.Balanced.DeletionLaw.DeletionSet line 12
  5. def OAI.Balanced.DeletionLaw.IsSubprobabilityKernel line 14
  6. def OAI.Balanced.DeletionLaw.deletionSet line 17
  7. def OAI.Balanced.DeletionLaw.DistinctOutput line 20
  8. def OAI.Balanced.DeletionLaw.CylinderBound line 23
  9. def OAI.Balanced.DeletionLaw.offsetAverage line 28
  10. def OAI.Balanced.DeletionLaw.successMass line 31
  11. def OAI.Balanced.DeletionLaw.deletionMass line 34
  12. def OAI.Balanced.DeletionLaw.conditionedDeletionMass line 37
  13. def OAI.Balanced.DeletionLaw.uniformDeletionMass line 40
  14. def OAI.Balanced.DeletionLaw.uniformDeletionLaw line 43
  15. def OAI.Balanced.DeletionLaw.FiniteDomination line 46
  16. def OAI.Balanced.DeletionLaw.ExponentialDomination line 54