OAI/Combinatorics/BalancedRyser/Deletion/Deletion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.IsDeletionSet line 19
  2. def OAI.Balanced.DeletionSet line 22
  3. instance OAI.Balanced.(instance at line 25) line 25
  4. instance OAI.Balanced.(instance at line 29) line 29
  5. def OAI.Balanced.uncoveredBy line 31
  6. def OAI.Balanced.deletionMultiplicity line 34
  7. def OAI.Balanced.empiricalMultiplicityMass line 37
  8. def OAI.Balanced.deletionPoissonMass line 41
  9. def OAI.Balanced.deletionMultiplicityTV line 44
  10. def OAI.Balanced.uniformDeletionMass line 47
  11. def OAI.Balanced.DeletionDominated line 50
  12. def OAI.Balanced.deletionEventProbability line 54
  13. def OAI.Balanced.deletionEventCard line 59
  14. def OAI.Balanced.exceptionalOccupancyLines line 63
  15. def OAI.Balanced.BadCoreCover line 70
  16. def OAI.Balanced.UniformDeletionVanishing line 75
  17. def OAI.Balanced.RobustDeletionResult line 84