`OAI/NumberTheory/DukePrimeDegree/Entropy/`

709 declarations, 0 contain sorry, 0 declared as axioms; 212 files

Files

AdaptiveFutureLifts.lean 3 declarations
AtomicFutureCover.lean 1 declarations
AtomicRootEntropy.lean 4 declarations
AtomicRootEntropyZero.lean 1 declarations
AuxiliaryKernelEntropy.lean 2 declarations
AuxiliaryPredecessorEntropy.lean 3 declarations
AuxiliaryRootInformation.lean 1 declarations
BilateralConditionalSupport.lean 6 declarations
BilateralFiniteCodes.lean 13 declarations
BoundedFutureMass.lean 2 declarations
BoundedFutureObservation.lean 2 declarations
BranchingCoverFuture.lean 1 declarations
BranchingStationaryObservation.lean 1 declarations
BranchingSubordinateObservation.lean 2 declarations
CompactFutureLifts.lean 3 declarations
CompactSmallObservations.lean 1 declarations
ConditionalBaseEmbedding.lean 1 declarations
ConditionalFiberRecoding.lean 3 declarations
ConditionalInformation.lean 2 declarations
ConditionalInformationClipping.lean 3 declarations
ConditionalInformationLowerBound.lean 2 declarations
ConditionalMapEntropy.lean 3 declarations
ConditionalNameCovers.lean 3 declarations
ConditionalPairs.lean 9 declarations
ConditionalProduct.lean 2 declarations
ConditionalRectangleProducts.lean 3 declarations
ConditionalSigmaLimit.lean 2 declarations
ConditionalSigmaOrder.lean 3 declarations
ConditioningFiniteLabels.lean 5 declarations
ContractingCutItineraries.lean 4 declarations
ControlledCoverFuture.lean 1 declarations
ControlledCutObservation.lean 4 declarations
ControlledRootFuture.lean 1 declarations
ControlledSubordinateObservation.lean 1 declarations
ConullFiberEntropyOrder.lean 3 declarations
CountableAuxiliaryEntropy.lean 5 declarations
CountableBoundaryEntropy.lean 10 declarations
CountableConditionalInformation.lean 2 declarations
CountableConditioningChain.lean 3 declarations
CountableFutureCodes.lean 10 declarations
CountableFutureConditioning.lean 6 declarations
CountableFutureFiberEntropy.lean 2 declarations
CountableFutureInformation.lean 2 declarations
CountableFutureMap.lean 8 declarations
CountableFutureSigma.lean 2 declarations
CountableObservationInformation.lean 4 declarations
CountablePatchEntropy.lean 2 declarations
CountableShannonInformation.lean 6 declarations
CountableSparseFineObservation.lean 1 declarations
CoverFutureObservation.lean 1 declarations
CoverPredecessorPacking.lean 2 declarations
DiagonalConditionalEntropy.lean 2 declarations
DiagonalEntropy.lean 4 declarations
EncodedObservationEntropy.lean 1 declarations
Entropy.lean 9 declarations
EntropyBalance.lean 6 declarations
EntropyCover.lean 2 declarations
EntropyGraph.lean 4 declarations
EntropyInverse.lean 5 declarations
EntropyUpper.lean 3 declarations
ExponentialPredecessorScales.lean 4 declarations
FineReturnObservation.lean 1 declarations
FiniteBlockEntropy.lean 9 declarations
FiniteFactorInformation.lean 3 declarations
FiniteFutureCodes.lean 8 declarations
FiniteLabelEntropy.lean 3 declarations
FiniteLabelInformation.lean 2 declarations
FiniteLevelFutureLifts.lean 2 declarations
FinitePatchEntropy.lean 1 declarations
FinitePatchNames.lean 1 declarations
FinitePrefixChartCodes.lean 1 declarations
FirstReturnPartition.lean 12 declarations
FirstRootConditionalProduct.lean 6 declarations
FourthIterateEntropy.lean 6 declarations
FutureAtomCovariance.lean 2 declarations
FutureBlockConditionalInformation.lean 4 declarations
FutureBlockInformation.lean 4 declarations
FutureClipEntropy.lean 1 declarations
FutureFiberEntropy.lean 3 declarations
FutureFiberInformation.lean 1 declarations
FutureFiberKernel.lean 12 declarations
FutureFiberMeasurability.lean 2 declarations
FutureFiberProbability.lean 1 declarations
FutureKernelCovariance.lean 7 declarations
FutureLabelBlocks.lean 7 declarations
FutureRestrictionNull.lean 1 declarations
FutureShiftBounds.lean 2 declarations
FutureSigmaAlgebra.lean 5 declarations
GlobalFutureKernelConstancy.lean 1 declarations
HeightObservationEntropy.lean 7 declarations
IncreasingConditioningChain.lean 2 declarations
IndependentAtomicConditional.lean 2 declarations
IndependentConditionalEntropy.lean 1 declarations
InfiniteFutureStationarity.lean 4 declarations
InfiniteLabelEntropy.lean 3 declarations
InfiniteLabelProbability.lean 1 declarations
KernelFutureInformation.lean 2 declarations
LastActiveEntropy.lean 2 declarations
LastActiveObservation.lean 11 declarations
LayeredCoverPredecessors.lean 1 declarations
LayeredObservations.lean 5 declarations
LayeredPredecessors.lean 2 declarations
LocalFutureKernelConstancy.lean 3 declarations
LowEntropyCollision.lean 2 declarations
LowEntropyHeightObservation.lean 1 declarations
LowEntropyInvariant.lean 1 declarations
LowEntropyRadialHeight.lean 1 declarations
LowEntropySubordinateObservation.lean 1 declarations
LowEntropySupportReduction.lean 1 declarations
MetricEntropy.lean 5 declarations
NameErrorEntropy.lean 7 declarations
NestedRealConditionals.lean 2 declarations
NeutralFiberNames.lean 4 declarations
NeutralFutureCoordinates.lean 3 declarations
NeutralNameCovers.lean 2 declarations
NeutralPatchFuturePair.lean 1 declarations
NeutralRelativeEntropy.lean 4 declarations
NeutralSubordinateObservation.lean 1 declarations
ObservationInformation.lean 7 declarations
PeriodicEntropyZero.lean 7 declarations
PhysicalWindowConditionals.lean 4 declarations
PredecessorEntropyLimit.lean 3 declarations
PredecessorEntropySum.lean 3 declarations
PredecessorFutureInformation.lean 2 declarations
PredecessorInformation.lean 2 declarations
PredecessorInformationBound.lean 1 declarations
PredecessorSymbols.lean 2 declarations
PredecessorWholeFutureEntropy.lean 6 declarations
PredecessorWholeFutureSigma.lean 10 declarations
PredecessorWordEntropy.lean 2 declarations
PredecessorWordEquivalence.lean 1 declarations
PrefixPointConditionals.lean 3 declarations
PrefixRootConditionals.lean 4 declarations
RadialFutureLifts.lean 4 declarations
RareLabelEntropy.lean 6 declarations
RareTernaryEntropy.lean 7 declarations
RefinedReturnEntropy.lean 2 declarations
RefinedReturnPartition.lean 7 declarations
RegularEntropyDischarge.lean 7 declarations
RegularEntropyScaling.lean 2 declarations
RegularEntropyTests.lean 10 declarations
RegularRootEntropyActual.lean 2 declarations
RegularRootEntropyLower.lean 2 declarations
RegularRootEntropySandwich.lean 8 declarations
RegularRootEntropyUpper.lean 2 declarations
RemainingConditionalIdentification.lean 1 declarations
RemainingExpansionInformation.lean 3 declarations
RemainingFutureInformation.lean 1 declarations
RemainingFutureShift.lean 5 declarations
RemainingLeafInformation.lean 2 declarations
ReturnCellEntropy.lean 1 declarations
ReturnObservationInformation.lean 2 declarations
ReturnPartitionEntropy.lean 2 declarations
RobustFiniteObservations.lean 4 declarations
RootAdaptedObservations.lean 12 declarations
RootFactorConditionalProduct.lean 3 declarations
RootInformationBound.lean 1 declarations
RootInformationGrowth.lean 2 declarations
RootInformationIntegral.lean 5 declarations
RootInformationScale.lean 4 declarations
RootItineraryMass.lean 6 declarations
RootOrderConditionals.lean 2 declarations
RootPredecessorInformation.lean 2 declarations
RootPredecessorWords.lean 2 declarations
RootPrefixAmbientFuture.lean 2 declarations
RootPrefixCountableInformation.lean 3 declarations
RootPrefixFiniteEntropy.lean 1 declarations
RootPrefixFutureEntropy.lean 1 declarations
RootPrefixFutureFibers.lean 7 declarations
RootPrefixFutureInformation.lean 1 declarations
RootPrefixFutureIntegral.lean 1 declarations
RootPrefixFutureMass.lean 5 declarations
RootPrefixFutureStationarity.lean 4 declarations
RootPrefixLocalConditionals.lean 2 declarations
RootPrefixSelfConditional.lean 1 declarations
RootPrefixTubeInformation.lean 4 declarations
RootProductInformation.lean 4 declarations
RowConditionalCompatibility.lean 5 declarations
SelfConditionalKernel.lean 5 declarations
SelfConditionalKernelMap.lean 2 declarations
ShiftedFactorConditionals.lean 3 declarations
ShiftedRootConditionalProduct.lean 1 declarations
SmallFineReturnObservation.lean 2 declarations
SmallFutureObservation.lean 1 declarations
SmallHeightEntropy.lean 1 declarations
SmallReturnEntropy.lean 2 declarations
SmallReturnPartition.lean 5 declarations
SmallSectionFutureObservation.lean 1 declarations
SparseFineObservation.lean 1 declarations
SparseObservationEntropy.lean 4 declarations
StationaryCoverObservation.lean 1 declarations
StationaryFiberConditioning.lean 3 declarations
StationaryFutureObservation.lean 1 declarations
SubexponentialCoverAlphabet.lean 5 declarations
SubordinateFutureBoxes.lean 2 declarations
SummablePartitionBoundaries.lean 8 declarations
UpperRootConditionalEntropy.lean 1 declarations
UpperRootCutItineraries.lean 3 declarations
UpperRootFutureEntropy.lean 1 declarations
UpperRootFutureFibers.lean 5 declarations
VaryingCutItinerary.lean 1 declarations
WeylEntropy.lean 4 declarations
WeylRootInformation.lean 4 declarations
WholeFutureBoxCover.lean 2 declarations
WholeFutureChain.lean 3 declarations
WholeFutureConditionalInformation.lean 4 declarations
WholeFutureCountableCover.lean 4 declarations
WholeFutureEntropyCriterion.lean 1 declarations
WholeFutureProbabilityKernel.lean 10 declarations
WholeFutureSelfConditional.lean 1 declarations
WholeFutureStationarity.lean 1 declarations
ZeroEntropyAllRoots.lean 2 declarations