OAI/Combinatorics/BalancedRyser/Profiles/Profile.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Profile line 15
  2. def OAI.Balanced.IsBoundedProfile line 17
  3. def OAI.Balanced.deletionInvisible line 22
  4. def OAI.Balanced.coverInvisible line 25
  5. def OAI.Balanced.deletionVisible line 28
  6. def OAI.Balanced.coverVisible line 29
  7. def OAI.Balanced.lineMultiplicity line 33
  8. def OAI.Balanced.planeProfile line 36
  9. def OAI.Balanced.lineProfile line 41
  10. def OAI.Balanced.profileDirac line 46
  11. def OAI.Balanced.empiricalProfileMeasure line 49
  12. def OAI.Balanced.IsProfilePair line 54
  13. abbrev OAI.Balanced.ProfileClass line 59
  14. def OAI.Balanced.ProfileClassValid line 63
  15. def OAI.Balanced.ProfileClassSizeGap line 67
  16. def OAI.Balanced.ProfileSequenceLimit line 72
  17. def OAI.Balanced.ProfileVisibleExcess line 82
  18. def OAI.Balanced.uniformProfileWitnessProbability line 93
  19. def OAI.Balanced.ProfileCountingResult line 100