OAI/Combinatorics/SquareDifference/
1803 declarations, 0 contain sorry, 0 declared as axioms; 81 files
Files
- ActualIntervalPair.lean 1 declarations
- AffineTuples.lean 41 declarations
- BlockAverage.lean 6 declarations
- BlockParameters.lean 8 declarations
- CRTTransfer.lean 8 declarations
- CircleDistance.lean 64 declarations
- CompleteWeights.lean 72 declarations
- ConductorBounds.lean 42 declarations
- CrossProducts.lean 50 declarations
- CyclicIndicator.lean 9 declarations
- DualCoordinates.lean 46 declarations
- Endpoint.lean 13 declarations
- EulerBudget.lean 4 declarations
- ExceptionalBasics.lean 10 declarations
- ExceptionalBudget.lean 6 declarations
- ExtendedPair.lean 4 declarations
- FiniteKernel.lean 47 declarations
- FourierLift.lean 101 declarations
- FunctionalSplit.lean 7 declarations
- GateExpansion.lean 10 declarations
- GaussSum.lean 29 declarations
- GoodPairSupport.lean 1 declarations
- InductionParameters.lean 5 declarations
- InductiveBounds.lean 2 declarations
- IntervalCoefficient.lean 6 declarations
- IntervalContraction.lean 2 declarations
- IntervalCounting.lean 5 declarations
- IntervalCrude.lean 3 declarations
- IntervalLift.lean 14 declarations
- IntervalPair.lean 3 declarations
- IntervalTransfer.lean 1 declarations
- IntervalTruncation.lean 14 declarations
- LiftMoments.lean 50 declarations
- LocalizedPair.lean 4 declarations
- LowProduct.lean 3 declarations
- Main.lean 7 declarations
- MarkedTuples.lean 48 declarations
- MatrixBounds.lean 54 declarations
- MixedCrude.lean 2 declarations
- MixedEnergy.lean 26 declarations
- MixedTransfer.lean 5 declarations
- OrderedBlock.lean 5 declarations
- OrderedGlobal.lean 2 declarations
- OrderedLow.lean 3 declarations
- OrderedRates.lean 7 declarations
- OutsideFourier.lean 12 declarations
- PairBridge.lean 18 declarations
- PhaseBounds.lean 29 declarations
- PositiveResidue.lean 10 declarations
- PowerParameters.lean 27 declarations
- PrimaryKernel.lean 36 declarations
- PrimeExtension.lean 10 declarations
- PrimeGauss.lean 35 declarations
- PrimeSetup.lean 19 declarations
- ProductBounds.lean 31 declarations
- RationalApproximation.lean 28 declarations
- RationalLift.lean 101 declarations
- ReflectionLaw.lean 47 declarations
- ResidueFourier.lean 39 declarations
- ResidueLift.lean 44 declarations
- ResidueReindex.lean 9 declarations
- RootModels.lean 34 declarations
- ScaleTransfer.lean 30 declarations
- SelectedPair.lean 3 declarations
- SelectedRoots.lean 4 declarations
- SievedFourier.lean 44 declarations
- SmallGood.lean 10 declarations
- SmallRoots.lean 7 declarations
- TensorLaw.lean 9 declarations
- TensorPair.lean 12 declarations
- TransferParameters.lean 6 declarations
- TransferRates.lean 7 declarations
- TupleEnergy.lean 63 declarations
- TupleReflection.lean 48 declarations
- TupleWeights.lean 51 declarations
- UniformBase.lean 3 declarations
- UniformInduction.lean 2 declarations
- UniformRates.lean 34 declarations
- UniformTransfer.lean 4 declarations
- WalshMoments.lean 50 declarations
- WordReflection.lean 37 declarations