OAI/NumberTheory/CubicGram/
687 declarations, 0 contain sorry, 0 declared as axioms; 45 files
Files
- CharacterGram.lean 4 declarations
- CommonFactors.lean 13 declarations
- CommonRows.lean 19 declarations
- Conjugation.lean 21 declarations
- Coordinates.lean 17 declarations
- CubeEstimates.lean 18 declarations
- CubeExtraction.lean 12 declarations
- CubicOperator.lean 29 declarations
- Definitions.lean 21 declarations
- DyadicRecurrence.lean 15 declarations
- EuclideanDomain.lean 15 declarations
- FrequencyGauss.lean 13 declarations
- FullCubeExtraction.lean 9 declarations
- GaussCharacters.lean 18 declarations
- GlobalRecurrence.lean 15 declarations
- GramCommon.lean 2 declarations
- GramDyad.lean 10 declarations
- GramMellin.lean 6 declarations
- GramNormalize.lean 3 declarations
- GramPoisson.lean 24 declarations
- InnerExtension.lean 19 declarations
- IntegerBasis.lean 18 declarations
- Jacobi.lean 15 declarations
- LatticeCounts.lean 10 declarations
- LatticePoisson.lean 37 declarations
- Main.lean 44 imports, no declarations
- MellinDecay.lean 31 declarations
- MellinNorm.lean 15 declarations
- MixedPoisson.lean 12 declarations
- Mobius.lean 9 declarations
- NormRecurrence.lean 12 declarations
- PeriodicPoisson.lean 21 declarations
- Periodization.lean 29 declarations
- PoissonBounds.lean 12 declarations
- PrimaryNormalization.lean 26 declarations
- PrimeFactors.lean 11 declarations
- QuantitativeRecurrence.lean 8 declarations
- Reciprocity.lean 17 declarations
- ReciprocityKernel.lean 12 declarations
- ResidueCharacters.lean 15 declarations
- SieveBase.lean 3 declarations
- SieveExponent.lean 11 declarations
- SieveImprovement.lean 16 declarations
- SieveMajorant.lean 13 declarations
- SquarefreeGauss.lean 31 declarations