OAI/Analysis/FiniteFactor/OrbitSampling/
256 declarations, 0 contain sorry, 0 declared as axioms; 54 files
Files
- CompactTorus.lean 8 declarations
- CrossProducts.lean 4 declarations
- Cube.lean 10 declarations
- CutoffMass.lean 4 declarations
- CylinderBasis.lean 2 declarations
- CylinderSystem.lean 6 declarations
- DiagonalContribution.lean 6 declarations
- DiagonalEvent.lean 4 declarations
- DiagonalIntegral.lean 2 declarations
- DiagonalLimit.lean 5 declarations
- Discrepancy.lean 4 declarations
- EmpiricalL2.lean 4 declarations
- Error.lean 7 declarations
- ErrorEvent.lean 4 declarations
- FirstCorrelation.lean 2 declarations
- FirstMarginal.lean 2 declarations
- Fourier.lean 4 declarations
- IdealProduct.lean 8 declarations
- IdealRectangleLimit.lean 5 declarations
- LambdaMarginals.lean 6 declarations
- LambdaMass.lean 3 declarations
- LambdaRectangles.lean 5 declarations
- LimitMeasure.lean 10 declarations
- Measures.lean 9 declarations
- Moments.lean 2 declarations
- OrbitSupport.lean 4 declarations
- OrderedRestriction.lean 10 declarations
- PairMoments.lean 2 declarations
- PhaseSelfMoment.lean 2 declarations
- Powers.lean 9 declarations
- ProductError.lean 4 declarations
- ProductMoments.lean 5 declarations
- RationalTests.lean 9 declarations
- RectangleApproximation.lean 1 declarations
- RectangleError.lean 3 declarations
- RotationTransport.lean 4 declarations
- SecondCorrelation.lean 2 declarations
- SecondMarginal.lean 3 declarations
- SelfMoment.lean 3 declarations
- SelfSummability.lean 5 declarations
- SingleCorrelation.lean 3 declarations
- Tail.lean 5 declarations
- TestedMarginals.lean 4 declarations
- TestedTransport.lean 5 declarations
- TorusLimitMarginals.lean 4 declarations
- TorusMarginals.lean 4 declarations
- TorusSupport.lean 9 declarations
- TriangleLaw.lean 3 declarations
- TrimmedMarginals.lean 2 declarations
- TrimmedWeak.lean 6 declarations
- UniformEvent.lean 2 declarations
- WeakLimit.lean 4 declarations
- WeightedTail.lean 2 declarations
- Weights.lean 11 declarations