OAI/Combinatorics/RamseyFive/Entropy/
1088 declarations, 0 contain sorry, 0 declared as axioms; 143 files
Files
- AllWindowCost.lean 4 declarations
- BandCoreRanks.lean 3 declarations
- BaseAlphabetCost.lean 3 declarations
- BaseFiniteCost.lean 8 declarations
- BaseMessageCost.lean 1 declarations
- BlockReveal.lean 22 declarations
- BlockSelected.lean 17 declarations
- CapDecoder.lean 7 declarations
- ChronologicalCapDomination.lean 6 declarations
- ClassExtraction.lean 6 declarations
- ClassSelection.lean 19 declarations
- ClippedWeight.lean 6 declarations
- CollisionSampling.lean 23 declarations
- ConditionPullback.lean 9 declarations
- ConditionalSampling.lean 8 declarations
- ContextDescription.lean 6 declarations
- CountedExtraction.lean 13 declarations
- DegreeCountFour.lean 2 declarations
- DeletionNumerics.lean 2 declarations
- DescriptionClean.lean 4 declarations
- DimensionThreePairs.lean 8 declarations
- EmptyWeight.lean 8 declarations
- EntropyCrossEntropy.lean 8 declarations
- EventMass.lean 18 declarations
- EventWeight.lean 11 declarations
- EventuallyHighPolyCost.lean 2 declarations
- EvictionDrift.lean 6 declarations
- FinalMarking.lean 4 declarations
- FinalValidationBudget.lean 1 declarations
- FiniteGrowth.lean 13 declarations
- FiniteKernels.lean 25 declarations
- FiniteNodeCost.lean 2 declarations
- FiniteNodeProcess.lean 4 declarations
- FinitePiLaw.lean 24 declarations
- FlagAlphabetLogs.lean 9 declarations
- FreshProcess.lean 2 declarations
- FreshPublicFamily.lean 12 declarations
- GenericFreshCost.lean 8 declarations
- GoodEndpoints.lean 9 declarations
- GoodIndexThreshold.lean 3 declarations
- GoodPairScores.lean 6 declarations
- GoodRepresentative.lean 11 declarations
- GuardedNodeCost.lean 3 declarations
- GuardedNodeOriginal.lean 11 declarations
- High.lean 5 declarations
- HighBudgetPoly.lean 3 declarations
- HighEndpointCutoffs.lean 16 declarations
- HighEntropyNumerics.lean 1 declarations
- HighExceptions.lean 10 declarations
- HighMomentBudget.lean 4 declarations
- History.lean 3 declarations
- HistoryCylinder.lean 26 declarations
- Hits.lean 15 declarations
- IIDLowerTail.lean 6 declarations
- IndependentLaw.lean 4 declarations
- IndependentSampling.lean 11 declarations
- IndependentTargetLoss.lean 6 declarations
- IndexMul.lean 2 declarations
- IteratedBudgets.lean 7 declarations
- Law.lean 20 declarations
- LevelCellSubset.lean 2 declarations
- LevelDensity.lean 2 declarations
- LevelTreeTrims.lean 7 declarations
- LocalNodeLaw.lean 7 declarations
- LogContractionDrop.lean 3 declarations
- LogSum.lean 20 declarations
- LowBudgetPoly.lean 5 declarations
- LowMomentBudget.lean 3 declarations
- Map.lean 18 declarations
- MapFst.lean 18 declarations
- MarkedActualBudget.lean 9 declarations
- MarkingBudget.lean 2 declarations
- MarkingNumerics.lean 3 declarations
- MeanTreeFailure.lean 3 declarations
- MessageCounting.lean 5 declarations
- MessageWeights.lean 4 declarations
- MetadataAlphabet.lean 11 declarations
- MetadataBudget.lean 5 declarations
- MomentWeightedCover.lean 2 declarations
- MultiplicityBudgets.lean 2 declarations
- OptionComposition.lean 3 declarations
- OptionEventBounds.lean 3 declarations
- OrderedExtraction.lean 9 declarations
- OrderedReciprocalLaw.lean 14 declarations
- OrderedRetention.lean 3 declarations
- OrderedWindowVariation.lean 2 declarations
- OrientedFiniteCost.lean 1 declarations
- OrientedTreeCost.lean 4 declarations
- OriginalHistoryPrivate.lean 2 declarations
- OriginalLevelLaw.lean 8 declarations
- OriginalMarginalLaw.lean 7 declarations
- OriginalUniformWeightedScoreMoment.lean 2 declarations
- Pairs.lean 4 declarations
- PermissibleLevels.lean 14 declarations
- PreRoundDeletion.lean 6 declarations
- PreparedWindows.lean 6 declarations
- PrimitiveMessageWeights.lean 19 declarations
- ProductHistory.lean 9 declarations
- PublicComposition.lean 4 declarations
- ReadyFailure.lean 2 declarations
- ReciprocalCodeNumerics.lean 3 declarations
- ReciprocalLossBudget.lean 5 declarations
- ReciprocalSupports.lean 3 declarations
- Rectangle.lean 22 declarations
- RecursivePlane.lean 2 declarations
- RelationMassCrossed.lean 1 declarations
- Repair.lean 6 declarations
- RepresentativeSet.lean 12 declarations
- RetainedCounters.lean 7 declarations
- RevealDomains.lean 25 declarations
- RevealMarginalDeficit.lean 2 declarations
- ReverseMessageCost.lean 5 declarations
- ScoreFiniteCost.lean 10 declarations
- SelectedRestriction.lean 3 declarations
- SequentialLaw.lean 12 declarations
- SmallFiniteCost.lean 1 declarations
- SplitLaw.lean 21 declarations
- StageNumerics.lean 3 declarations
- SubsetDeficit.lean 9 declarations
- SubsetEncoding.lean 15 declarations
- SubsetMixture.lean 14 declarations
- Swap.lean 6 declarations
- Tail.lean 12 declarations
- TargetAverage.lean 4 declarations
- TargetLoss.lean 4 declarations
- ThreeHeader.lean 2 declarations
- TreeOmissionBound.lean 3 declarations
- TreeWeights.lean 10 declarations
- TwoCapCost.lean 3 declarations
- UniformCutoff.lean 11 declarations
- UniformHistory.lean 19 declarations
- UnionMarking.lean 15 declarations
- UniversalFreshCost.lean 3 declarations
- UnusedRepresentative.lean 17 declarations
- ValidationBudgetWide.lean 2 declarations
- VariableTreeCost.lean 1 declarations
- WeightedLowHits.lean 3 declarations
- WindowBudgetNumerics.lean 1 declarations
- WindowLossAggregation.lean 2 declarations
- WindowPosterior.lean 9 declarations
- WindowReadiness.lean 3 declarations
- WindowTargetInputs.lean 4 declarations
- WindowVariation.lean 4 declarations