OAI/NumberTheory/Ostmann/Supply/
984 declarations, 0 contain sorry, 0 declared as axioms; 178 files
Files
- ActualCenteredBudget.lean 3 declarations
- ActualCenteredBudgetSupport.lean 11 declarations
- ActualKernelAverage.lean 2 declarations
- ActualKernelBudget.lean 4 declarations
- ActualKernelPairSum.lean 3 declarations
- ActualLogBudget.lean 3 declarations
- ActualPrimeLower.lean 3 declarations
- ActualPrimeMeanError.lean 2 declarations
- ActualPrimeUpper.lean 1 declarations
- ActualWindowSizes.lean 1 declarations
- AveragedKernelPairing.lean 5 declarations
- BalancedKernelBlocks.lean 4 declarations
- BalancedProjectionBlocks.lean 2 declarations
- BilinearCube.lean 7 declarations
- BilinearCubeSupport.lean 4 declarations
- BivariateTruncation.lean 18 declarations
- BlockNorm.lean 2 declarations
- BoundaryCoverage.lean 2 declarations
- BoundaryCoverageCounts.lean 2 declarations
- BoundaryCoverageFinite.lean 4 declarations
- BoundaryCoverageScale.lean 1 declarations
- BoundaryCoverageWeightScale.lean 4 declarations
- CRTPrimitiveEnergy.lean 21 declarations
- CenteredBudget.lean 7 declarations
- CenteredCoordinateSupport.lean 7 declarations
- CenteredOrthogonality.lean 4 declarations
- CenteredPrimitiveEnergy.lean 13 declarations
- CenteredProjection.lean 11 declarations
- CenteredProjectionPairing.lean 2 declarations
- CenteredRamanujanKernel.lean 3 declarations
- CenteredResidueProjection.lean 6 declarations
- CenteredSupportProjection.lean 9 declarations
- CollisionLogImbalance.lean 2 declarations
- CollisionPrimeCellBudget.lean 4 declarations
- CompletionArithmetic.lean 7 declarations
- CompletionCounting.lean 8 declarations
- CompletionInterchange.lean 5 declarations
- CompletionWeights.lean 9 declarations
- ConcreteExtensionWeights.lean 2 declarations
- ConcreteSubsetEnergyBudget.lean 2 declarations
- ConductorBounds.lean 10 declarations
- ConstantModeBudget.lean 2 declarations
- ContractingKernel.lean 4 declarations
- ContractionConstants.lean 9 declarations
- CoverageMargin.lean 2 declarations
- ElementaryPolynomial.lean 6 declarations
- EnumeratedTailSieveEnergy.lean 1 declarations
- FavorableMassAlternative.lean 3 declarations
- FavorableTailPrimeMass.lean 1 declarations
- FiniteConvolution.lean 6 declarations
- FiniteCoordinateEnergy.lean 9 declarations
- FiniteCoverage.lean 18 declarations
- FiniteParseval.lean 9 declarations
- FiniteSpectralProjection.lean 11 declarations
- FiniteTensorKernel.lean 4 declarations
- Fourier.lean 13 declarations
- FourierIsometry.lean 6 declarations
- FourierKernel.lean 4 declarations
- FourierKernelBounds.lean 5 declarations
- GoodSieveMultipliers.lean 2 declarations
- GroupedCharacters.lean 4 declarations
- GroupedCharactersBound.lean 4 declarations
- GroupedCharactersError.lean 2 declarations
- GroupedCharactersExpBound.lean 2 declarations
- GroupedCharactersFamily.lean 9 declarations
- GroupedCharactersPrimitive.lean 11 declarations
- GroupedCharactersPrimitiveBound.lean 6 declarations
- GroupedCharactersReindex.lean 6 declarations
- GroupedCharactersSupport.lean 9 declarations
- GroupedCharactersTransform.lean 13 declarations
- GroupedPrimitiveCharacters.lean 12 declarations
- GroupedPrimitiveCharactersConductor.lean 3 declarations
- GroupedPrimitiveCharactersLift.lean 10 declarations
- GroupedPrimitiveCharactersProduct.lean 3 declarations
- IndexedMultiplierWeights.lean 5 declarations
- IntegerSparseSieve.lean 1 declarations
- KernelEmpirical.lean 8 declarations
- KernelMoments.lean 7 declarations
- KernelProducts.lean 7 declarations
- KernelScalarBounds.lean 6 declarations
- KernelSymmetry.lean 6 declarations
- KernelTensor.lean 8 declarations
- KernelTruncatedWeight.lean 4 declarations
- LocalBlock.lean 11 declarations
- LocalBlockBound.lean 1 declarations
- LocalBlockConstant.lean 7 declarations
- LocalKernelBlocks.lean 5 declarations
- LocalKernelCoordinates.lean 8 declarations
- LocalKernelOperator.lean 6 declarations
- LocalKernelPolynomial.lean 9 declarations
- LocalProjectionBlocks.lean 4 declarations
- LocalSparseKernelContraction.lean 1 declarations
- LocalSparsePolydisc.lean 1 declarations
- LogImbalanceVariance.lean 3 declarations
- LogRatioCauchy.lean 3 declarations
- MultiplierRatioProduct.lean 4 declarations
- MultiplierWeightedBudget.lean 10 declarations
- NaturalPrimeSupportSieve.lean 5 declarations
- NaturalResidueAverage.lean 3 declarations
- NaturalWeight.lean 5 declarations
- NonnegativeSparseWeight.lean 6 declarations
- NonsparseSupply.lean 1 declarations
- PolynomialFunctional.lean 9 declarations
- PrimeBandSelection.lean 2 declarations
- PrimeBandSelectionBalance.lean 4 declarations
- PrimeBandSelectionBudget.lean 3 declarations
- PrimeBandSelectionFinite.lean 5 declarations
- PrimeEnumeration.lean 9 declarations
- PrimeMeanBounds.lean 2 declarations
- PrimeMeanIdentity.lean 8 declarations
- PrimeMeanScale.lean 1 declarations
- PrimePowerTransfer.lean 4 declarations
- PrimePowerTransferBasic.lean 4 declarations
- PrimeSetSupportSieve.lean 1 declarations
- PrimeSubsetMainTerm.lean 1 declarations
- PrimeSubsetMass.lean 3 declarations
- PrimeSubsetProducts.lean 5 declarations
- PrimeSubsetSieve.lean 3 declarations
- PrimeSupportEnergy.lean 2 declarations
- PrimeSupportSieve.lean 2 declarations
- ProjectionCrossBound.lean 3 declarations
- ProjectionScalar.lean 4 declarations
- RawBlockBounds.lean 5 declarations
- ResidueBudgetScale.lean 2 declarations
- ResidueKernel.lean 5 declarations
- ResidueKernelNormBounds.lean 5 declarations
- ResidueProjectionScalar.lean 5 declarations
- ResidueProjectionSides.lean 4 declarations
- ResidueRatio.lean 10 declarations
- ResidueTensor.lean 3 declarations
- ResidueVectorNorm.lean 9 declarations
- RestrictedSubsetEnergy.lean 3 declarations
- RetainedBandProducts.lean 2 declarations
- RetainedBandScales.lean 6 declarations
- SieveBudgetParameters.lean 4 declarations
- SmoothPrimeWeight.lean 8 declarations
- SpectralApproximation.lean 8 declarations
- SpectralConcentration.lean 9 declarations
- SpectralProjection.lean 9 declarations
- SpectralProjectionAffine.lean 2 declarations
- SpectralProjectionPairing.lean 5 declarations
- SquarefreeEulerBound.lean 2 declarations
- SquarefreeMultiplierCount.lean 7 declarations
- Statement.lean 6 declarations
- SubsetEnergyAmplification.lean 2 declarations
- SubsetReducedEnergy.lean 4 declarations
- SupplyRadiusBounds.lean 3 declarations
- TailSieveEnergy.lean 2 declarations
- TailSieveParameters.lean 8 declarations
- TailSparsePairSum.lean 2 declarations
- TensorCoordinates.lean 9 declarations
- TensorKernel.lean 6 declarations
- TensorModeBudget.lean 5 declarations
- TensorModeDecomposition.lean 6 declarations
- TensorModeEnergy.lean 11 declarations
- TensorModeLocalKernel.lean 4 declarations
- TensorModePairing.lean 2 declarations
- TensorModePolynomial.lean 4 declarations
- TensorModeReflection.lean 9 declarations
- TensorModes.lean 22 declarations
- TensorOperators.lean 32 declarations
- TernaryProductPolynomial.lean 9 declarations
- TruncatedBilinearCube.lean 4 declarations
- TruncatedWeight.lean 8 declarations
- TruncationMargins.lean 4 declarations
- TruncationScale.lean 4 declarations
- UniformBalanced.lean 5 declarations
- UniformDecomposition.lean 5 declarations
- UniformNorms.lean 5 declarations
- UniformProjection.lean 6 declarations
- UnitKernelGenerating.lean 5 declarations
- UnitKernelMean.lean 4 declarations
- UnitProductSize.lean 4 declarations
- UnitWeightPolynomial.lean 7 declarations
- UnitWeightTruncation.lean 4 declarations
- WeightFiniteIndex.lean 4 declarations
- WeightPointwiseBound.lean 4 declarations
- WeightedMultiplierSupply.lean 3 declarations