OAI/NumberTheory/OrdinaryCorrelations/Elliott/
168 declarations, 0 contain sorry, 0 declared as axioms; 21 files
Files
- Adj.lean 26 declarations
- BiasedSequenceOfFailure.lean 1 declarations
- BinIndex.lean 4 declarations
- BinaryCorrectedElliott.lean 1 declarations
- Cesaro.lean 10 declarations
- CesaroNormFunctionEq.lean 3 declarations
- ConstantsA.lean 14 declarations
- DeletedOut.lean 6 declarations
- DirMatrix.lean 9 declarations
- DivisorForm.lean 5 declarations
- Main.lean 572 imports, no declarations
- MeanZeroOfNonpretentious.lean 4 declarations
- NormThreshold.lean 10 declarations
- OneAddSumLeProduct.lean 13 declarations
- PrimeDefect.lean 7 declarations
- ProductOneBounded.lean 12 declarations
- RelativeErrorTendsto.lean 2 declarations
- SmoothCutoffExists.lean 21 declarations
- SubsetCost.lean 6 declarations
- TraceMean.lean 4 declarations
- WeightMeanOneLe.lean 10 declarations