`OAI/Dynamics/EntropyCounterexample/`

1722 declarations, 0 contain sorry, 0 declared as axioms; 184 files

Files

AmbientPrediction.lean 12 declarations
AmbientRetraction.lean 34 declarations
AngularDerivative.lean 12 declarations
AngularExtension.lean 8 declarations
Assembly.lean 2 declarations
AttractionSupport.lean 2 imports, no declarations
C1Conjugacy.lean 3 declarations
C1CoordinatePullback.lean 6 declarations
C1Coordinates.lean 8 declarations
C1Retraction.lean 2 declarations
C1Support.lean 6 imports, no declarations
CircleClockDoubling.lean 15 declarations
CircleDoublingChains.lean 33 declarations
CircleWindingCocycle.lean 16 declarations
Clock.lean 50 declarations
ClockAtInfinity.lean 6 declarations
ClockCharts.lean 14 declarations
ClockDynamics.lean 15 declarations
ClockLift.lean 9 declarations
ClockLiftBridge.lean 4 declarations
ClockLocalExtension.lean 10 declarations
ClockModel.lean 18 declarations
ClockOrbit.lean 15 declarations
ClockPassage.lean 7 declarations
ClockPeriodization.lean 10 declarations
ClockPeriodizationCompatibility.lean 2 declarations
ClockPeriodizationLocal.lean 3 declarations
ClockPrediction.lean 10 declarations
ClockProfiles.lean 11 declarations
ClockQuotient.lean 19 declarations
ClockQuotientC1.lean 6 declarations
ClockRotation.lean 26 declarations
ClockSupport.lean 4 imports, no declarations
CompactLabels.lean 3 declarations
ConcreteContinuity.lean 5 declarations
ConcreteErasure.lean 4 declarations
ConcreteErasureLimit.lean 3 declarations
ConcreteInputRegularity.lean 19 declarations
Conjugacy.lean 7 declarations
CoordinateGoodCover.lean 24 declarations
Counterexample.lean 1 declarations
CounterexampleEntropy.lean 1 declarations
CylinderAttraction.lean 17 declarations
CylinderModels.lean 8 declarations
Definitions.lean 12 declarations
Development.lean 90 imports, no declarations
EigenpairBound.lean 3 declarations
Embedding.lean 10 declarations
EntropyBounds.lean 8 declarations
EntropyCoding.lean 9 declarations
EntropyLocalization.lean 9 declarations
EntropyNeighborhood.lean 2 declarations
EntropySection.lean 5 declarations
EntropySparseCover.lean 4 declarations
EntropySupport.lean 5 imports, no declarations
ExactSequenceSpectrum.lean 13 declarations
FiniteSpectrumBound.lean 3 declarations
FiniteTypeSupport.lean 3 imports, no declarations
GainCircle.lean 4 declarations
GainLocalExtension.lean 6 declarations
GainProfile.lean 7 declarations
GlobalEscape.lean 5 declarations
HomotopySpectrum.lean 4 declarations
ImageEntropy.lean 7 declarations
InfinityChart.lean 13 declarations
InputSeries.lean 5 declarations
LocalPredictionInput.lean 2 declarations
Map.lean 32 declarations
MapAmplification.lean 8 declarations
MapBoundedOrbit.lean 7 declarations
MapC1.lean 3 declarations
MapC1Complete.lean 2 declarations
MapClockComponent.lean 6 declarations
MapConcretePassage.lean 2 declarations
MapContinuity.lean 8 declarations
MapData.lean 20 declarations
MapEntropy.lean 3 declarations
MapEntropyComplete.lean 1 declarations
MapErasure.lean 10 declarations
MapFinalReduction.lean 5 declarations
MapFiniteOrbit.lean 6 declarations
MapGlobalEscape.lean 7 declarations
MapInfinity.lean 5 declarations
MapInfinityAttraction.lean 4 declarations
MapInputRegularity.lean 4 declarations
MapLocalEscape.lean 1 declarations
MapMainRegularity.lean 6 declarations
MapOrbitAlternatives.lean 3 declarations
MapOrbitLift.lean 17 declarations
MapPassage.lean 9 declarations
MapPassagePhase.lean 8 declarations
MapPassageSchedule.lean 5 declarations
MapPrediction.lean 3 declarations
MapPredictionAgreement.lean 9 declarations
MapPreparationRadius.lean 3 declarations
MapPreparationReset.lean 4 declarations
MapQuotientContinuity.lean 8 declarations
MapReadout.lean 3 declarations
MapRecoveredReadout.lean 6 declarations
MapRegisterRegularity.lean 6 declarations
MapRegularity.lean 6 declarations
MapSignal.lean 16 declarations
MapSignals.lean 9 declarations
MapTerminalEntropy.lean 11 declarations
ModelTransport.lean 4 imports, no declarations
MonotoneItineraries.lean 7 declarations
NormalizedPrediction.lean 8 declarations
OnePointSupport.lean 5 declarations
OrbitAttraction.lean 18 declarations
OrbitSupport.lean 29 imports, no declarations
OrderedIntervalLabels.lean 5 declarations
PassagePhase.lean 10 declarations
PassagePhaseInterval.lean 8 declarations
PeriodicDerivativeBound.lean 3 declarations
PeriodicEntropy.lean 5 declarations
PhaseAlignment.lean 13 declarations
PolarLabels.lean 2 declarations
PolarProductEntropy.lean 6 declarations
PolynomialSpectralBound.lean 22 declarations
PredictionClock.lean 13 declarations
PredictionDerivative.lean 5 declarations
PredictionInput.lean 7 declarations
PredictionModelBridge.lean 11 declarations
PredictionSeries.lean 4 declarations
PredictionSignal.lean 3 declarations
PredictionSupport.lean 4 imports, no declarations
PredictionTerm.lean 9 declarations
RadialOrbitRepresentation.lean 17 declarations
RadialRegisterEntropy.lean 4 declarations
RawBaseGoodCover.lean 2 declarations
RawInvariantInfinity.lean 11 declarations
RawInvariantSets.lean 15 declarations
RawSpectrumFactor.lean 13 declarations
ReadoutCover.lean 26 declarations
ReadoutLocalExtension.lean 11 declarations
RealAngularDerivative.lean 7 declarations
RealizedConstruction.lean 20 declarations
RealizedRegisterRegularity.lean 4 declarations
RegisterEmbedded.lean 3 declarations
RegisterEntropyCoding.lean 5 declarations
RegisterEntropySupport.lean 1 import, no declarations
RegisterErasure.lean 9 declarations
RegisterInterval.lean 3 declarations
RegisterLinearity.lean 12 declarations
RegisterReset.lean 5 declarations
Saturation.lean 33 declarations
SaturationEntropy.lean 5 declarations
SkewProduct.lean 14 declarations
SmallCoverNaturality.lean 18 declarations
SparseLogBound.lean 8 declarations
SparseVisits.lean 11 declarations
SpectralRadius.lean 5 declarations
SphereAngularInput.lean 32 declarations
SphereAngularTransport.lean 5 declarations
SphereChartLimits.lean 10 declarations
SphereCharts.lean 42 declarations
SphereCompactSupport.lean 5 declarations
SphereCompactSupportParam.lean 2 declarations
SphereCoverGeometry.lean 28 declarations
SphereCutoffBounds.lean 5 declarations
SphereCutoffSupport.lean 2 imports, no declarations
SphereCutoffTransport.lean 8 declarations
SphereCutoffs.lean 25 declarations
SphereCutoffsAffine.lean 27 declarations
SphereDoubling.lean 27 declarations
SphereDoublingCharts.lean 7 declarations
SphereGeometry.lean 9 imports, no declarations
SphereInfinityChart.lean 27 declarations
SphereMainUpdate.lean 17 declarations
SphereMainUpdateTransport.lean 4 declarations
SphereOverlapDoubling.lean 11 declarations
SpherePerturbation.lean 8 declarations
SpherePolynomialPerturbation.lean 37 declarations
SphereSquareEquator.lean 22 declarations
SphereSquareFiber.lean 10 declarations
SphereTranslation.lean 22 declarations
StandardRegisterUpdate.lean 7 declarations
StandardSaturation.lean 10 declarations
TargetReduction.lean 1 declarations
TerminalEntropySupport.lean 14 imports, no declarations
TopologicalAttraction.lean 8 declarations
TopologyCoverSupport.lean 3 imports, no declarations
TranslationC1.lean 5 declarations
TranslationDerivative.lean 10 declarations