OAI/Combinatorics/BalancedRyser/Local/Local.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.TupleCode line 19
  2. abbrev OAI.Balanced.Local.ChoiceCode line 21
  3. abbrev OAI.Balanced.Local.Output line 22
  4. def OAI.Balanced.Local.decodeTuple line 24
  5. def OAI.Balanced.Local.decodeChoice line 25
  6. def OAI.Balanced.Local.configuration line 27
  7. def OAI.Balanced.Local.constituentMultiplicity line 32
  8. def OAI.Balanced.Local.logBudget line 36
  9. def OAI.Balanced.Local.offsetProbability line 38
  10. def OAI.Balanced.Local.conditionedOffsetProbability line 42
  11. structure OAI.Balanced.Local.RetentionRule line 45
  12. abbrev OAI.Balanced.Local.Kernel line 53
  13. def OAI.Balanced.Local.KernelConditions line 55
  14. def OAI.Balanced.Local.selectedProbability line 66
  15. def OAI.Balanced.Local.generatorUnionAt line 71
  16. def OAI.Balanced.Local.reuseCount line 75
  17. structure OAI.Balanced.Local.EqualityPattern line 78
  18. abbrev OAI.Balanced.Local.DirectionAssignment line 85
  19. abbrev OAI.Balanced.Local.Bits line 87
  20. def OAI.Balanced.Local.Eligible line 89
  21. def OAI.Balanced.Local.prescribedTuple line 94
  22. def OAI.Balanced.Local.prescribedPoint line 98
  23. def OAI.Balanced.Local.Aligned line 103
  24. def OAI.Balanced.Local.Admissible line 108
  25. def OAI.Balanced.Local.prescribedDesignated line 116
  26. def OAI.Balanced.Local.prescribedPartners line 120
  27. def OAI.Balanced.Local.piecePoints line 127
  28. def OAI.Balanced.Local.AllowedPiece line 132
  29. def OAI.Balanced.Local.BadCover line 139
  30. def OAI.Balanced.Local.AdmissibleBadCover line 147
  31. def OAI.Balanced.Local.PencilLocalResult line 152
  32. def OAI.Balanced.Local.PencilReuseResult line 160
  33. def OAI.Balanced.Local.AlignmentNormalizationResult line 168
  34. def OAI.Balanced.Local.PencilSmallReuseResult line 175
  35. def OAI.Balanced.Local.PencilTwoReusesResult line 185