OAI/NumberTheory/DirichletL/QuadraticSieve/
1180 declarations, 0 contain sorry, 0 declared as axioms; 36 files
Files
- AnnularLifting.lean 44 declarations
- AnnularRecursion.lean 51 declarations
- CoefficientCancellation.lean 35 declarations
- CommonMasks.lean 32 declarations
- CoprimeBilinearBound.lean 43 declarations
- CrossSeparation.lean 28 declarations
- CuspCoercivity.lean 44 declarations
- DivisorBlocks.lean 35 declarations
- DualMiddleExpansion.lean 27 declarations
- DyadicColumns.lean 36 declarations
- FiniteOperator.lean 53 declarations
- GcdReduction.lean 40 declarations
- GlobalBinLoss.lean 30 declarations
- GreenIntegrals.lean 33 declarations
- HighKernelGeometry.lean 39 declarations
- IdealQuotients.lean 35 declarations
- InitialBound.lean 46 declarations
- LogarithmicLoss.lean 23 declarations
- LogarithmicSectors.lean 19 declarations
- MainTermDifference.lean 38 declarations
- MaskedPrincipalBounds.lean 22 declarations
- MiddleWindows.lean 19 declarations
- PoissonComparison.lean 29 declarations
- PoissonConstants.lean 15 declarations
- PrimePools.lean 44 declarations
- PrincipalDifference.lean 24 declarations
- PrincipalMajorants.lean 22 declarations
- PrincipalTruncation.lean 27 declarations
- ProductColumns.lean 22 declarations
- RetainedDualBounds.lean 23 declarations
- SelectedExponents.lean 49 declarations
- SpatialDerivatives.lean 46 declarations
- SquareParts.lean 34 declarations
- TruncatedSecondTransfer.lean 19 declarations
- UniformTailBounds.lean 22 declarations
- UnrestrictedCharacters.lean 32 declarations