OAI/Dynamics/EntropyCounterexample.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 264 imports below, so a file that imports it gets all of them.
Imports
- OAI.Dynamics.EntropyCounterexample.AmbientPrediction
- OAI.Dynamics.EntropyCounterexample.AmbientRetraction
- OAI.Dynamics.EntropyCounterexample.AngularDerivative
- OAI.Dynamics.EntropyCounterexample.AngularExtension
- OAI.Dynamics.EntropyCounterexample.Assembly
- OAI.Dynamics.EntropyCounterexample.AttractionSupport
- OAI.Dynamics.EntropyCounterexample.C1Conjugacy
- OAI.Dynamics.EntropyCounterexample.C1CoordinatePullback
- OAI.Dynamics.EntropyCounterexample.C1Coordinates
- OAI.Dynamics.EntropyCounterexample.C1Retraction
- OAI.Dynamics.EntropyCounterexample.C1Support
- OAI.Dynamics.EntropyCounterexample.CircleClockDoubling
- OAI.Dynamics.EntropyCounterexample.CircleDoublingChains
- OAI.Dynamics.EntropyCounterexample.CircleWindingCocycle
- OAI.Dynamics.EntropyCounterexample.Clock
- OAI.Dynamics.EntropyCounterexample.ClockAtInfinity
- OAI.Dynamics.EntropyCounterexample.ClockCharts
- OAI.Dynamics.EntropyCounterexample.ClockDynamics
- OAI.Dynamics.EntropyCounterexample.ClockLift
- OAI.Dynamics.EntropyCounterexample.ClockLiftBridge
- OAI.Dynamics.EntropyCounterexample.ClockLocalExtension
- OAI.Dynamics.EntropyCounterexample.ClockModel
- OAI.Dynamics.EntropyCounterexample.ClockOrbit
- OAI.Dynamics.EntropyCounterexample.ClockPassage
- OAI.Dynamics.EntropyCounterexample.ClockPeriodization
- OAI.Dynamics.EntropyCounterexample.ClockPeriodizationCompatibility
- OAI.Dynamics.EntropyCounterexample.ClockPeriodizationLocal
- OAI.Dynamics.EntropyCounterexample.ClockPrediction
- OAI.Dynamics.EntropyCounterexample.ClockProfiles
- OAI.Dynamics.EntropyCounterexample.ClockQuotient
- OAI.Dynamics.EntropyCounterexample.ClockQuotientC1
- OAI.Dynamics.EntropyCounterexample.ClockRotation
- OAI.Dynamics.EntropyCounterexample.ClockSupport
- OAI.Dynamics.EntropyCounterexample.CompactLabels
- OAI.Dynamics.EntropyCounterexample.ConcreteContinuity
- OAI.Dynamics.EntropyCounterexample.ConcreteErasure
- OAI.Dynamics.EntropyCounterexample.ConcreteErasureLimit
- OAI.Dynamics.EntropyCounterexample.ConcreteInputRegularity
- OAI.Dynamics.EntropyCounterexample.Conjugacy
- OAI.Dynamics.EntropyCounterexample.CoordinateGoodCover
- OAI.Dynamics.EntropyCounterexample.Counterexample
- OAI.Dynamics.EntropyCounterexample.CounterexampleEntropy
- OAI.Dynamics.EntropyCounterexample.CylinderAttraction
- OAI.Dynamics.EntropyCounterexample.CylinderModels
- OAI.Dynamics.EntropyCounterexample.Definitions
- OAI.Dynamics.EntropyCounterexample.Development
- OAI.Dynamics.EntropyCounterexample.EigenpairBound
- OAI.Dynamics.EntropyCounterexample.Embedding
- OAI.Dynamics.EntropyCounterexample.EntropyBounds
- OAI.Dynamics.EntropyCounterexample.EntropyCoding
- OAI.Dynamics.EntropyCounterexample.EntropyLocalization
- OAI.Dynamics.EntropyCounterexample.EntropyNeighborhood
- OAI.Dynamics.EntropyCounterexample.EntropySection
- OAI.Dynamics.EntropyCounterexample.EntropySparseCover
- OAI.Dynamics.EntropyCounterexample.EntropySupport
- OAI.Dynamics.EntropyCounterexample.ExactSequenceSpectrum
- OAI.Dynamics.EntropyCounterexample.FiniteSpectrumBound
- OAI.Dynamics.EntropyCounterexample.FiniteTypeSupport
- OAI.Dynamics.EntropyCounterexample.GainCircle
- OAI.Dynamics.EntropyCounterexample.GainLocalExtension
- OAI.Dynamics.EntropyCounterexample.GainProfile
- OAI.Dynamics.EntropyCounterexample.GlobalEscape
- OAI.Dynamics.EntropyCounterexample.HomotopySpectrum
- OAI.Dynamics.EntropyCounterexample.ImageEntropy
- OAI.Dynamics.EntropyCounterexample.InfinityChart
- OAI.Dynamics.EntropyCounterexample.InputSeries
- OAI.Dynamics.EntropyCounterexample.LocalPredictionInput
- OAI.Dynamics.EntropyCounterexample.Map
- OAI.Dynamics.EntropyCounterexample.MapAmplification
- OAI.Dynamics.EntropyCounterexample.MapBoundedOrbit
- OAI.Dynamics.EntropyCounterexample.MapC1
- OAI.Dynamics.EntropyCounterexample.MapC1Complete
- OAI.Dynamics.EntropyCounterexample.MapClockComponent
- OAI.Dynamics.EntropyCounterexample.MapConcretePassage
- OAI.Dynamics.EntropyCounterexample.MapContinuity
- OAI.Dynamics.EntropyCounterexample.MapData
- OAI.Dynamics.EntropyCounterexample.MapEntropy
- OAI.Dynamics.EntropyCounterexample.MapEntropyComplete
- OAI.Dynamics.EntropyCounterexample.MapErasure
- OAI.Dynamics.EntropyCounterexample.MapFinalReduction
- OAI.Dynamics.EntropyCounterexample.MapFiniteOrbit
- OAI.Dynamics.EntropyCounterexample.MapGlobalEscape
- OAI.Dynamics.EntropyCounterexample.MapInfinity
- OAI.Dynamics.EntropyCounterexample.MapInfinityAttraction
- OAI.Dynamics.EntropyCounterexample.MapInputRegularity
- OAI.Dynamics.EntropyCounterexample.MapLocalEscape
- OAI.Dynamics.EntropyCounterexample.MapMainRegularity
- OAI.Dynamics.EntropyCounterexample.MapOrbitAlternatives
- OAI.Dynamics.EntropyCounterexample.MapOrbitLift
- OAI.Dynamics.EntropyCounterexample.MapPassage
- OAI.Dynamics.EntropyCounterexample.MapPassagePhase
- OAI.Dynamics.EntropyCounterexample.MapPassageSchedule
- OAI.Dynamics.EntropyCounterexample.MapPrediction
- OAI.Dynamics.EntropyCounterexample.MapPredictionAgreement
- OAI.Dynamics.EntropyCounterexample.MapPreparationRadius
- OAI.Dynamics.EntropyCounterexample.MapPreparationReset
- OAI.Dynamics.EntropyCounterexample.MapQuotientContinuity
- OAI.Dynamics.EntropyCounterexample.MapReadout
- OAI.Dynamics.EntropyCounterexample.MapRecoveredReadout
- OAI.Dynamics.EntropyCounterexample.MapRegisterRegularity
- OAI.Dynamics.EntropyCounterexample.MapRegularity
- OAI.Dynamics.EntropyCounterexample.MapSignal
- OAI.Dynamics.EntropyCounterexample.MapSignals
- OAI.Dynamics.EntropyCounterexample.MapTerminalEntropy
- OAI.Dynamics.EntropyCounterexample.ModelTransport
- OAI.Dynamics.EntropyCounterexample.MonotoneItineraries
- OAI.Dynamics.EntropyCounterexample.NormalizedPrediction
- OAI.Dynamics.EntropyCounterexample.OnePointSupport
- OAI.Dynamics.EntropyCounterexample.OrbitAttraction
- OAI.Dynamics.EntropyCounterexample.OrbitSupport
- OAI.Dynamics.EntropyCounterexample.OrderedIntervalLabels
- OAI.Dynamics.EntropyCounterexample.PassagePhase
- OAI.Dynamics.EntropyCounterexample.PassagePhaseInterval
- OAI.Dynamics.EntropyCounterexample.PeriodicDerivativeBound
- OAI.Dynamics.EntropyCounterexample.PeriodicEntropy
- OAI.Dynamics.EntropyCounterexample.PhaseAlignment
- OAI.Dynamics.EntropyCounterexample.PolarLabels
- OAI.Dynamics.EntropyCounterexample.PolarProductEntropy
- OAI.Dynamics.EntropyCounterexample.PolynomialSpectralBound
- OAI.Dynamics.EntropyCounterexample.PredictionClock
- OAI.Dynamics.EntropyCounterexample.PredictionDerivative
- OAI.Dynamics.EntropyCounterexample.PredictionInput
- OAI.Dynamics.EntropyCounterexample.PredictionModelBridge
- OAI.Dynamics.EntropyCounterexample.PredictionSeries
- OAI.Dynamics.EntropyCounterexample.PredictionSignal
- OAI.Dynamics.EntropyCounterexample.PredictionSupport
- OAI.Dynamics.EntropyCounterexample.PredictionTerm
- OAI.Dynamics.EntropyCounterexample.RadialOrbitRepresentation
- OAI.Dynamics.EntropyCounterexample.RadialRegisterEntropy
- OAI.Dynamics.EntropyCounterexample.RawBaseGoodCover
- OAI.Dynamics.EntropyCounterexample.RawInvariantInfinity
- OAI.Dynamics.EntropyCounterexample.RawInvariantSets
- OAI.Dynamics.EntropyCounterexample.RawSpectrumFactor
- OAI.Dynamics.EntropyCounterexample.ReadoutCover
- OAI.Dynamics.EntropyCounterexample.ReadoutLocalExtension
- OAI.Dynamics.EntropyCounterexample.RealAngularDerivative
- OAI.Dynamics.EntropyCounterexample.RealizedConstruction
- OAI.Dynamics.EntropyCounterexample.RealizedRegisterRegularity
- OAI.Dynamics.EntropyCounterexample.RegisterEmbedded
- OAI.Dynamics.EntropyCounterexample.RegisterEntropyCoding
- OAI.Dynamics.EntropyCounterexample.RegisterEntropySupport
- OAI.Dynamics.EntropyCounterexample.RegisterErasure
- OAI.Dynamics.EntropyCounterexample.RegisterInterval
- OAI.Dynamics.EntropyCounterexample.RegisterLinearity
- OAI.Dynamics.EntropyCounterexample.RegisterReset
- OAI.Dynamics.EntropyCounterexample.Saturation
- OAI.Dynamics.EntropyCounterexample.SaturationEntropy
- OAI.Dynamics.EntropyCounterexample.SkewProduct
- OAI.Dynamics.EntropyCounterexample.SmallCoverNaturality
- OAI.Dynamics.EntropyCounterexample.SparseLogBound
- OAI.Dynamics.EntropyCounterexample.SparseVisits
- OAI.Dynamics.EntropyCounterexample.SpectralRadius
- OAI.Dynamics.EntropyCounterexample.SphereAngularInput
- OAI.Dynamics.EntropyCounterexample.SphereAngularTransport
- OAI.Dynamics.EntropyCounterexample.SphereChartLimits
- OAI.Dynamics.EntropyCounterexample.SphereCharts
- OAI.Dynamics.EntropyCounterexample.SphereCompactSupport
- OAI.Dynamics.EntropyCounterexample.SphereCompactSupportParam
- OAI.Dynamics.EntropyCounterexample.SphereCoverGeometry
- OAI.Dynamics.EntropyCounterexample.SphereCutoffBounds
- OAI.Dynamics.EntropyCounterexample.SphereCutoffSupport
- OAI.Dynamics.EntropyCounterexample.SphereCutoffTransport
- OAI.Dynamics.EntropyCounterexample.SphereCutoffs
- OAI.Dynamics.EntropyCounterexample.SphereCutoffsAffine
- OAI.Dynamics.EntropyCounterexample.SphereDoubling
- OAI.Dynamics.EntropyCounterexample.SphereDoublingCharts
- OAI.Dynamics.EntropyCounterexample.SphereGeometry
- OAI.Dynamics.EntropyCounterexample.SphereInfinityChart
- OAI.Dynamics.EntropyCounterexample.SphereMainUpdate
- OAI.Dynamics.EntropyCounterexample.SphereMainUpdateTransport
- OAI.Dynamics.EntropyCounterexample.SphereOverlapDoubling
- OAI.Dynamics.EntropyCounterexample.SpherePerturbation
- OAI.Dynamics.EntropyCounterexample.SpherePolynomialPerturbation
- OAI.Dynamics.EntropyCounterexample.SphereSquareEquator
- OAI.Dynamics.EntropyCounterexample.SphereSquareFiber
- OAI.Dynamics.EntropyCounterexample.SphereTranslation
- OAI.Dynamics.EntropyCounterexample.StandardRegisterUpdate
- OAI.Dynamics.EntropyCounterexample.StandardSaturation
- OAI.Dynamics.EntropyCounterexample.TargetReduction
- OAI.Dynamics.EntropyCounterexample.TerminalEntropySupport
- OAI.Dynamics.EntropyCounterexample.TopologicalAttraction
- OAI.Dynamics.EntropyCounterexample.TopologyCoverSupport
- OAI.Dynamics.EntropyCounterexample.TranslationC1
- OAI.Dynamics.EntropyCounterexample.TranslationDerivative
- OAI.Geometry.SingularHomology.ActualSingularSubdivision
- OAI.Geometry.SingularHomology.ActualSingularSubdivisionMap
- OAI.Geometry.SingularHomology.AffineSimplexCone
- OAI.Geometry.SingularHomology.AffineSimplexGeometry
- OAI.Geometry.SingularHomology.AffineSingularRealization
- OAI.Geometry.SingularHomology.BarycentricSubdivision
- OAI.Geometry.SingularHomology.ChainComplexTransport
- OAI.Geometry.SingularHomology.ChainMapRangeLift
- OAI.Geometry.SingularHomology.CircleHomologySupport
- OAI.Geometry.SingularHomology.CoordinateHomology
- OAI.Geometry.SingularHomology.FiniteCoverHomology
- OAI.Geometry.SingularHomology.FiniteCoverHomologyRawBase
- OAI.Geometry.SingularHomology.FiniteGoodCoverHomology
- OAI.Geometry.SingularHomology.FiniteSimplicialHomology
- OAI.Geometry.SingularHomology.HomologyConjugacy
- OAI.Geometry.SingularHomology.HomologyConstant
- OAI.Geometry.SingularHomology.HomologyCycle
- OAI.Geometry.SingularHomology.HomologyEigenvalue
- OAI.Geometry.SingularHomology.HomologyEmpty
- OAI.Geometry.SingularHomology.HomologyEvaluation
- OAI.Geometry.SingularHomology.HomologyHomotopyEquiv
- OAI.Geometry.SingularHomology.HomologyNaturality
- OAI.Geometry.SingularHomology.HomologySpectrumFactor
- OAI.Geometry.SingularHomology.HomologySupport
- OAI.Geometry.SingularHomology.HomologyTransfer
- OAI.Geometry.SingularHomology.HomologyZero
- OAI.Geometry.SingularHomology.IteratedSubdivision
- OAI.Geometry.SingularHomology.IteratedSubdivisionMesh
- OAI.Geometry.SingularHomology.MapHomology
- OAI.Geometry.SingularHomology.MapRealizedHomology
- OAI.Geometry.SingularHomology.RecursiveSubdivisionMesh
- OAI.Geometry.SingularHomology.SimplexSingularCompatibility
- OAI.Geometry.SingularHomology.SimplexSingularRealization
- OAI.Geometry.SingularHomology.SimplexSubdivisionMesh
- OAI.Geometry.SingularHomology.SimplexSubtypeMesh
- OAI.Geometry.SingularHomology.SimplicialMayerVietoris
- OAI.Geometry.SingularHomology.SimplicialSphereHomology
- OAI.Geometry.SingularHomology.SingularAcyclicModels
- OAI.Geometry.SingularHomology.SingularAugmentation
- OAI.Geometry.SingularHomology.SingularChainFoundations
- OAI.Geometry.SingularHomology.SingularChainInclusion
- OAI.Geometry.SingularHomology.SingularChainsFinsupp
- OAI.Geometry.SingularHomology.SingularChainsFinsuppBoundary
- OAI.Geometry.SingularHomology.SingularCoverChains
- OAI.Geometry.SingularHomology.SingularCoverNaturality
- OAI.Geometry.SingularHomology.SingularCoverNaturalityExtended
- OAI.Geometry.SingularHomology.SingularCycleFilling
- OAI.Geometry.SingularHomology.SingularMayerVietorisSupport
- OAI.Geometry.SingularHomology.SingularRealizedSmallness
- OAI.Geometry.SingularHomology.SingularSimplexCircleLift
- OAI.Geometry.SingularHomology.SingularSimplexLebesgue
- OAI.Geometry.SingularHomology.SingularSmallChainSupport
- OAI.Geometry.SingularHomology.SingularSmallChains
- OAI.Geometry.SingularHomology.SingularSmallComparison
- OAI.Geometry.SingularHomology.SingularSmallNaturality
- OAI.Geometry.SingularHomology.SingularSubdivision
- OAI.Geometry.SingularHomology.SingularSubdivisionEventuallySmall
- OAI.Geometry.SingularHomology.SingularSubdivisionIterateRealization
- OAI.Geometry.SingularHomology.SingularSubdivisionSmallness
- OAI.Geometry.SingularHomology.SingularSubdivisionSupport
- OAI.Geometry.SingularHomology.SingularSupportNaturality
- OAI.Geometry.SingularHomology.SingularSupportedFilling
- OAI.Geometry.SingularHomology.SingularUniversalChainMap
- OAI.Geometry.SingularHomology.SingularUniversalFinsupp
- OAI.Geometry.SingularHomology.SingularUniversalOperator
- OAI.Geometry.SingularHomology.SkewProductHomology
- OAI.Geometry.SingularHomology.SmallCoverMayerVietoris
- OAI.Geometry.SingularHomology.SphereMayerVietorisEigen
- OAI.Geometry.SingularHomology.SphereSquareHomologyTransport
- OAI.Geometry.SingularHomology.SubdivisionQuasiIso
- OAI.Geometry.SingularHomology.SubdivisionSubtypeMesh
- OAI.Geometry.SingularHomology.SubdivisionSupport
- OAI.Geometry.SingularHomology.SubdivisionSupportMesh
- OAI.Geometry.SingularHomology.TetrahedronChainInjection
- OAI.Geometry.SingularHomology.TetrahedronGoodCover
- OAI.Geometry.SingularHomology.TetrahedronGoodCoverBundle
- OAI.Geometry.SingularHomology.TetrahedronHomologyEquiv
- OAI.Geometry.SingularHomology.TetrahedronHomologyRank
- OAI.Geometry.SingularHomology.TetrahedronRadialHomeomorph
- OAI.Geometry.SingularHomology.TetrahedronSingular