OAI/Analysis/MarkovType/
2139 declarations, 0 contain sorry, 0 declared as axioms; 212 files
Files
- All.lean 5 imports, no declarations
- AlternatingNorm.lean 37 declarations
- AntitoneSeminormLimit.lean 11 declarations
- C00FiniteCoordinates.lean 7 declarations
- ChartAveraging.lean 4 declarations
- ChartChain.lean 3 declarations
- ChartPathProbability.lean 23 declarations
- ChartTransport.lean 34 declarations
- ClassicalRenorming.lean 2 declarations
- CoefficientBasic.lean 6 declarations
- CoefficientBlockGain.lean 3 declarations
- CoefficientBlockIteration.lean 2 declarations
- CoefficientBlockPartition.lean 2 declarations
- CoefficientConsecutiveBlocks.lean 5 declarations
- CoefficientFunctional.lean 3 declarations
- CoefficientGrid.lean 3 declarations
- CoefficientLowerPower.lean 4 declarations
- CoefficientQuotientGain.lean 1 declarations
- CoefficientSelectedBlocks.lean 10 declarations
- CoefficientSequenceOps.lean 19 declarations
- CoefficientThresholdCount.lean 1 declarations
- CoefficientUpperBlocking.lean 5 declarations
- CoordinateFactorization.lean 1 declarations
- CoordinateRepresentability.lean 1 declarations
- CubeNotJConvex.lean 5 declarations
- DenseFiniteApproximation.lean 1 declarations
- DyadicBellman.lean 17 declarations
- DyadicBlockCoordinates.lean 12 declarations
- DyadicConvexPotential.lean 30 declarations
- DyadicCotypeDuality.lean 2 declarations
- DyadicIndependentBlocks.lean 13 declarations
- DyadicInterpolation.lean 8 declarations
- DyadicSmoothRenorming.lean 8 declarations
- DyadicSynthesisPairing.lean 4 declarations
- DyadicTree.lean 38 declarations
- DyadicTreeMartingale.lean 30 declarations
- DyadicWeakAmplification.lean 12 declarations
- DyadicWeakMaxDefinition.lean 1 declarations
- DyadicWeakMaxFromUpperL2.lean 4 declarations
- DyadicWeakType.lean 18 declarations
- EndNorm.lean 15 declarations
- FailureJApproximation.lean 5 declarations
- FailureJCounterexample.lean 5 declarations
- FailureJTriangular.lean 9 declarations
- FiniteAnnihilator.lean 4 declarations
- FiniteAveraging.lean 2 declarations
- FiniteBoundedEnergy.lean 7 declarations
- FiniteBoundedEnergyScale.lean 2 declarations
- FiniteChains.lean 9 declarations
- FiniteCharts.lean 6 declarations
- FiniteConditionalAverage.lean 39 declarations
- FiniteConditionalMartingale.lean 11 declarations
- FiniteCoordinateSupport.lean 1 declarations
- FiniteCoupling.lean 40 declarations
- FiniteCubeBound.lean 2 declarations
- FiniteDualNorming.lean 4 declarations
- FiniteDyadicMartingale.lean 24 declarations
- FiniteDyadicProbability.lean 20 declarations
- FiniteFirstCrossing.lean 10 declarations
- FiniteGeometricBands.lean 14 declarations
- FiniteGoldstine.lean 2 declarations
- FiniteIndependentCopies.lean 11 declarations
- FiniteL2.lean 10 declarations
- FiniteL2CoefficientAdapter.lean 13 declarations
- FiniteL2IsometryTransport.lean 6 declarations
- FiniteLowerL2Cotype.lean 2 declarations
- FiniteMarcinkiewicz.lean 29 declarations
- FiniteMartingaleBasic.lean 18 declarations
- FiniteMartingaleConditional.lean 8 declarations
- FiniteMartingaleDuality.lean 3 declarations
- FiniteMartingaleExtrapolation.lean 2 declarations
- FiniteMartingaleMaximal.lean 2 declarations
- FiniteMartingalePairing.lean 8 declarations
- FiniteMartingaleTransport.lean 13 declarations
- FiniteMatching.lean 3 declarations
- FiniteNormApproximation.lean 3 declarations
- FinitePaths.lean 24 declarations
- FinitePowerIntegrals.lean 8 declarations
- FinitePowerMeanBound.lean 1 declarations
- FinitePredictableSelection.lean 11 declarations
- FinitePredictableTransform.lean 18 declarations
- FiniteProbability.lean 7 declarations
- FiniteRamsey.lean 6 declarations
- FiniteRepresentation.lean 1 declarations
- FiniteSelectionCompression.lean 8 declarations
- FiniteSelectionCounter.lean 23 declarations
- FiniteSeparation.lean 11 declarations
- FiniteSmoothMoments.lean 11 declarations
- FiniteStoppingTime.lean 12 declarations
- FiniteTailAmplification.lean 4 declarations
- FiniteTailCorrection.lean 17 declarations
- FiniteTruncationTail.lean 5 declarations
- FiniteWalk.lean 7 declarations
- FiniteWalkCoordinates.lean 8 declarations
- FiniteWalkMoment.lean 1 declarations
- FiniteWalkWitness.lean 1 declarations
- FiniteWeightedHolder.lean 5 declarations
- FinitelyRepresentable.lean 8 declarations
- FinitelyRepresentableEmbedding.lean 2 declarations
- ForwardBound.lean 1 declarations
- FourLetters.lean 21 declarations
- GeometricThresholdPowerSum.lean 3 declarations
- HomogeneousPotential.lean 13 declarations
- HomogeneousRows.lean 7 declarations
- IntegerCocycle.lean 29 declarations
- InterleavedCuts.lean 7 declarations
- JConvexityBasic.lean 21 declarations
- JConvexityFiniteRepresentability.lean 2 declarations
- JConvexityReflexivity.lean 3 declarations
- JConvexityScalarSquares.lean 5 declarations
- JConvexitySquareAverage.lean 5 declarations
- JamesCubeImprovement.lean 11 declarations
- JamesEnflo.lean 6 declarations
- LatticeCosts.lean 3 declarations
- LatticeCubes.lean 20 declarations
- LatticeLift.lean 24 declarations
- LatticePaths.lean 18 declarations
- Main.lean 5 declarations
- MarkedChains.lean 11 declarations
- MarkedLetters.lean 6 declarations
- MarkedMoments.lean 2 declarations
- MarkedPaths.lean 26 declarations
- MarkovFiniteRepresentability.lean 3 declarations
- MarkovObstruction.lean 1 declarations
- MarkovReflexivity.lean 3 declarations
- MarkovRenorming.lean 4 declarations
- MarkovTransport.lean 5 declarations
- MidpointPotential.lean 2 declarations
- NormCompression.lean 9 declarations
- NormedC00.lean 10 declarations
- OddEdgeTransfer.lean 2 declarations
- OrbitDisplacement.lean 18 declarations
- OrderedBoundedCubes.lean 11 declarations
- OrderedCoordinates.lean 11 declarations
- OrderedJColumns.lean 12 declarations
- OrderedMarkovTransfer.lean 2 declarations
- OrderedNorm.lean 10 declarations
- OrderedNormConstruction.lean 1 declarations
- OrderedNormStructural.lean 1 declarations
- OrderedSequences.lean 17 declarations
- PeriodicArcs.lean 52 declarations
- PeriodicOrderIso.lean 45 declarations
- PisierPowerRenorming.lean 1 declarations
- PowerConvexity.lean 1 declarations
- PowerGrowth.lean 2 declarations
- PowerRenormingFromDyadic.lean 12 declarations
- PowerSmoothness.lean 3 declarations
- PrefixBlocks.lean 18 declarations
- PrefixIndicators.lean 12 declarations
- Renormed.lean 21 declarations
- RenormedGeometry.lean 5 declarations
- RenormingBasic.lean 12 declarations
- RepresentationDistortion.lean 1 declarations
- ReversibleMartingales.lean 30 declarations
- ScalarPowerRemainder.lean 4 declarations
- ScalarUltralimit.lean 26 declarations
- SelectedRows.lean 11 declarations
- SeminormUltralimit.lean 5 declarations
- SeminormUniformApproximation.lean 2 declarations
- SequenceL2JConvex.lean 8 declarations
- SmoothMarkovType.lean 5 declarations
- SmoothRenormed.lean 6 declarations
- SmoothnessBounds.lean 28 declarations
- SpreadingConstruction.lean 4 declarations
- SpreadingCoordinateEmbedding.lean 2 declarations
- SpreadingLimit.lean 15 declarations
- SpreadingLimitCauchy.lean 6 declarations
- SpreadingLimitDiagonal.lean 2 declarations
- SpreadingLimitEmbedding.lean 6 declarations
- SpreadingLimitReal.lean 3 declarations
- SpreadingLimitUniform.lean 2 declarations
- SpreadingModel.lean 4 declarations
- StructuralL2Estimates.lean 6 declarations
- SubdivisionAverage.lean 16 declarations
- SubdivisionInvariantBlocks.lean 8 declarations
- SubdivisionLimit.lean 16 declarations
- SubdivisionMergeConvex.lean 13 declarations
- SubdivisionMergeCoordinates.lean 7 declarations
- SubdivisionNearIsometry.lean 5 declarations
- SubdivisionOperators.lean 44 declarations
- SubdivisionOrderedNorm.lean 9 declarations
- SubdivisionProfileDefs.lean 6 declarations
- SubdivisionProfileExpansion.lean 4 declarations
- SubdivisionProfiles.lean 5 declarations
- SubdivisionSameSign.lean 3 declarations
- SubdivisionSpreading.lean 7 declarations
- TailMoment.lean 3 declarations
- TriangularArrays.lean 4 declarations
- TriangularBasic.lean 5 declarations
- TriangularCompletion.lean 13 declarations
- TriangularCoordinateEmbeddings.lean 2 declarations
- TriangularCounterexample.lean 2 declarations
- TriangularLimitSeminorm.lean 20 declarations
- TriangularNonreflexivity.lean 12 declarations
- TriangularPrefix.lean 8 declarations
- TriangularQuotient.lean 2 declarations
- TriangularReflexivity.lean 6 declarations
- TriangularRepresentability.lean 2 declarations
- TriangularTransport.lean 8 declarations
- TwoLevels.lean 17 declarations
- UniformSmoothNonsquare.lean 7 declarations
- WalkDisplacement.lean 5 declarations
- WalkDrift.lean 19 declarations
- WalkLabels.lean 19 declarations
- WalkLandmarks.lean 20 declarations
- WalkMarkedDisplacement.lean 11 declarations
- WalkParameters.lean 19 declarations
- WalkPrefixLevels.lean 8 declarations
- WalkTransport.lean 20 declarations
- WeightedEvents.lean 11 declarations
- WordAction.lean 25 declarations
- WordReduction.lean 46 declarations