OAI/Combinatorics/SharpRamsey/Marking/
522 declarations, 0 contain sorry, 0 declared as axioms; 54 files
Files
- ActualClassLaw.lean 1 declarations
- AtomEscape.lean 24 declarations
- CardVectorLifts.lean 26 declarations
- ClassConditioning.lean 8 declarations
- ClassSelection.lean 5 declarations
- ClassStep.lean 2 declarations
- ClassTransport.lean 13 declarations
- CostContraction.lean 3 declarations
- ExcessCost.lean 3 declarations
- FinalMarking.lean 9 declarations
- GoodIndices.lean 5 declarations
- GoodRealization.lean 4 declarations
- GoodRound.lean 4 declarations
- GoodRows.lean 7 declarations
- HighGoodHistory.lean 2 declarations
- HighRank.lean 25 declarations
- HighRankBudgets.lean 9 declarations
- HighRankChoices.lean 3 declarations
- HighRankClass.lean 3 declarations
- HighRankConflict.lean 2 declarations
- HighRankContext.lean 3 declarations
- HighRankEndpoints.lean 10 declarations
- HighRankExperiment.lean 1 declarations
- HighRankOrdered.lean 1 declarations
- HighRankStep.lean 1 declarations
- HighRankStream.lean 1 declarations
- HighRankSuccess.lean 5 declarations
- MarkingActual.lean 23 declarations
- MarkingCaps.lean 8 declarations
- MarkingClassSelection.lean 7 declarations
- MarkingClassification.lean 4 declarations
- MarkingDeficit.lean 5 declarations
- MarkingFiniteClasses.lean 7 declarations
- MarkingMessage.lean 13 declarations
- MarkingOrientation.lean 36 declarations
- MarkingTwoCaps.lean 9 declarations
- MarkingTwoScans.lean 18 declarations
- MultiplicityClass.lean 6 declarations
- OrderedClassLaw.lean 8 declarations
- Popular.lean 51 declarations
- RawLowerTail.lean 18 declarations
- RootCost.lean 3 declarations
- RowSpan.lean 39 declarations
- SelectedStep.lean 3 declarations
- SelectionLogBound.lean 3 declarations
- StageBudget.lean 5 declarations
- StepCost.lean 1 declarations
- TailSum.lean 24 declarations
- TargetEvent.lean 33 declarations
- TrackedGeometry.lean 3 declarations
- TrackedSelection.lean 7 declarations
- TrackedStep.lean 5 declarations
- UniformStep.lean 1 declarations
- UniformSupports.lean 2 declarations