OAI/NumberTheory/DirichletL/CubicSieve/
1986 declarations, 0 contain sorry, 0 declared as axioms; 91 files
Files
- Algebra.lean 9 declarations
- AnnularImprovement.lean 1 declarations
- ArithmeticBins.lean 55 declarations
- B2Growth.lean 2 declarations
- Blocks.lean 4 declarations
- CanonicalLogEnergy.lean 33 declarations
- ChildTransfer.lean 32 declarations
- ClosedRecursion.lean 11 declarations
- ColumnShells.lean 6 declarations
- CommonFactorBound.lean 3 declarations
- CompactDescent.lean 8 declarations
- ConjugateProfiles.lean 41 declarations
- CostGrowth.lean 3 declarations
- CrossFactorization.lean 36 declarations
- CubeBlocks.lean 34 declarations
- CubeLabels.lean 47 declarations
- CutoffOrders.lean 31 declarations
- DensityBudgets.lean 35 declarations
- DescendantBounds.lean 4 declarations
- DescentEnergy.lean 2 declarations
- DivisorTargets.lean 17 declarations
- DualCoefficients.lean 6 declarations
- DualShell.lean 2 declarations
- DualZeroMode.lean 16 declarations
- Dyadic.lean 7 declarations
- DyadicKernel.lean 25 declarations
- Elements.lean 11 declarations
- ExponentImprovement.lean 6 declarations
- Extraction.lean 5 declarations
- ExtractionBounds.lean 5 declarations
- ExtractionOptimization.lean 7 declarations
- Factorization.lean 10 declarations
- FirstCoreCutoff.lean 19 declarations
- FirstPassage.lean 28 declarations
- FixedProfiles.lean 34 declarations
- FrequencyBlocks.lean 44 declarations
- FrequencyCutoffs.lean 46 declarations
- FrequencyDyads.lean 6 declarations
- FrequencyShell.lean 4 declarations
- FullExtraction.lean 5 declarations
- FullImprovement.lean 3 declarations
- FullNorm.lean 10 declarations
- Gauss.lean 13 declarations
- GaussNorm.lean 2 declarations
- Gcd.lean 11 declarations
- GlobalEncoding.lean 36 declarations
- Growth.lean 4 declarations
- Ideal.lean 18 declarations
- Initial.lean 16 declarations
- IntegratedTransfer.lean 42 declarations
- KernelEnergy.lean 34 declarations
- KernelTransfer.lean 1 declarations
- LiteralSources.lean 55 declarations
- LocalBrackets.lean 37 declarations
- LogSeparation.lean 40 declarations
- LogarithmicTargets.lean 27 declarations
- Majorant.lean 4 declarations
- Mobius.lean 15 declarations
- Norm.lean 3 declarations
- NormalizedMass.lean 32 declarations
- Operator.lean 13 declarations
- PaddedPassage.lean 46 declarations
- PairPoisson.lean 5 declarations
- PairPrimes.lean 11 declarations
- Poisson.lean 13 declarations
- PooledRows.lean 47 declarations
- PrincipalDensity.lean 34 declarations
- PrincipalNormalization.lean 26 declarations
- QuantitativePassage.lean 18 declarations
- QuotientColumns.lean 9 declarations
- RadialProfiles.lean 52 declarations
- RadialWindows.lean 40 declarations
- RankMargins.lean 22 declarations
- RayCoefficients.lean 47 declarations
- RayExpansion.lean 30 declarations
- Recurrence.lean 2 declarations
- ReopenedFibers.lean 44 declarations
- ReopeningBounds.lean 32 declarations
- ReopeningSeparation.lean 41 declarations
- ResidualSectors.lean 35 declarations
- RowCaps.lean 57 declarations
- RowMajorants.lean 64 declarations
- ScaleCaps.lean 51 declarations
- SecondPoisson.lean 28 declarations
- Sharp.lean 3 declarations
- Smoothed.lean 7 declarations
- SquarefreeTransfer.lean 12 declarations
- SupportNorms.lean 24 declarations
- TwistedProfiles.lean 55 declarations
- UniformTransfer.lean 13 declarations
- ZeroMode.lean 2 declarations