`OAI/Analysis/FiniteFactor/`

1473 declarations, 0 contain sorry, 0 declared as axioms; 271 files

Folders

BiasedPairs/ 8 files, 37 declarations
Coupling/ 23 files, 228 declarations
CrossedProduct/ 104 files, 528 declarations
Diffuse/ 8 files, 29 declarations
Fiber/ 6 files, 33 declarations
Matrix/ 5 files, 35 declarations
OrbitSampling/ 54 files, 256 declarations
Sampling/ 37 files, 179 declarations

Files

BoundedMatrixOperator.lean 17 declarations
CompactGraphLusin.lean 2 declarations
CompactZeroTransfer.lean 2 declarations
Contradiction.lean 8 declarations
Convolution.lean 14 declarations
CountableMaskedError.lean 2 declarations
FiniteMeasureCylinderCriterion.lean 1 declarations
FiniteMixtureAlgebra.lean 6 declarations
FiniteProductAbsoluteContinuity.lean 2 declarations
FiniteProductMixture.lean 10 declarations
FiniteSingleTag.lean 3 declarations
IndependentCount.lean 3 declarations
L2UniformAbsoluteContinuity.lean 2 declarations
Main.lean 1 declarations
Model.lean 5 declarations
OperatorTracialRepresentation.lean 17 declarations
OperatorUltraweak.lean 2 declarations
PeriodizedUniform.lean 6 declarations
Polynomial.lean 16 declarations
ProductDensityLimit.lean 5 declarations
ProductKernel.lean 5 declarations
Quasinilpotence.lean 3 declarations
SubmeasureL2Density.lean 1 declarations
TagExponentialLower.lean 2 declarations
TailEstimate.lean 5 declarations
Truncation.lean 8 declarations