OAI/NumberTheory/CubicMoment/Transform/
684 declarations, 0 contain sorry, 0 declared as axioms; 162 files
Files
- MetaplecticAbel.lean 11 declarations
- MetaplecticActualBlockMean.lean 1 declarations
- MetaplecticActualInverse.lean 3 declarations
- MetaplecticAngularOuter.lean 3 declarations
- MetaplecticAuxiliary.lean 11 declarations
- MetaplecticBilinear.lean 4 declarations
- MetaplecticBilinearMellin.lean 3 declarations
- MetaplecticBlockAmplitude.lean 6 declarations
- MetaplecticBlockCoefficient.lean 4 declarations
- MetaplecticBlockMean.lean 2 declarations
- MetaplecticCodeDyads.lean 10 declarations
- MetaplecticCodeMean.lean 4 declarations
- MetaplecticCodePartition.lean 9 declarations
- MetaplecticCoefficientDecay.lean 4 declarations
- MetaplecticCoefficientMajorant.lean 9 declarations
- MetaplecticCoefficientMass.lean 5 declarations
- MetaplecticCoefficientSeries.lean 9 declarations
- MetaplecticCommonBound.lean 4 declarations
- MetaplecticCompletedBox.lean 2 declarations
- MetaplecticCompletedLow.lean 4 declarations
- MetaplecticCompletedPoleBound.lean 3 declarations
- MetaplecticCompletedPolynomial.lean 4 declarations
- MetaplecticCompletedRadialMean.lean 1 declarations
- MetaplecticCompletedSeries.lean 7 declarations
- MetaplecticCompletedShort.lean 3 declarations
- MetaplecticCompletedTail.lean 1 declarations
- MetaplecticCompletion.lean 21 declarations
- MetaplecticCompletionCoefficient.lean 5 declarations
- MetaplecticConjugateMean.lean 8 declarations
- MetaplecticContinuationProof.lean 9 declarations
- MetaplecticCriticalFinite.lean 1 declarations
- MetaplecticCriticalKernel.lean 7 declarations
- MetaplecticCriticalTransform.lean 1 declarations
- MetaplecticCubeEnergy.lean 9 declarations
- MetaplecticCubeFiberSum.lean 2 declarations
- MetaplecticCubeMean.lean 4 declarations
- MetaplecticCutoffPowers.lean 7 declarations
- MetaplecticDecompletion.lean 4 declarations
- MetaplecticDualFinite.lean 7 declarations
- MetaplecticDualScaling.lean 4 declarations
- MetaplecticDualTailWeights.lean 6 declarations
- MetaplecticEulerFactor.lean 11 declarations
- MetaplecticEulerInverse.lean 2 declarations
- MetaplecticForwardCompletion.lean 1 declarations
- MetaplecticFreeBlock.lean 2 declarations
- MetaplecticFreeFrequency.lean 6 declarations
- MetaplecticFreeMean.lean 2 declarations
- MetaplecticFreeReflection.lean 2 declarations
- MetaplecticGammaRecurrence.lean 4 declarations
- MetaplecticGaussGrowth.lean 5 declarations
- MetaplecticGrowthProvider.lean 4 declarations
- MetaplecticHarmonic.lean 1 declarations
- MetaplecticHeight.lean 17 declarations
- MetaplecticInverseMean.lean 4 declarations
- MetaplecticInversePoleMean.lean 2 declarations
- MetaplecticInverseScale.lean 4 declarations
- MetaplecticInverseSplit.lean 3 declarations
- MetaplecticKernelIntegrability.lean 1 declarations
- MetaplecticLargeLow.lean 1 declarations
- MetaplecticLevelMass.lean 2 declarations
- MetaplecticLocalEuler.lean 10 declarations
- MetaplecticLocalSeries.lean 9 declarations
- MetaplecticLogCounting.lean 1 declarations
- MetaplecticLogTail.lean 3 declarations
- MetaplecticLongCard.lean 1 declarations
- MetaplecticLongCompletion.lean 2 declarations
- MetaplecticLongCounting.lean 2 declarations
- MetaplecticLongDyads.lean 10 declarations
- MetaplecticLongGeometry.lean 3 declarations
- MetaplecticLongSieve.lean 5 declarations
- MetaplecticLongSieveScale.lean 3 declarations
- MetaplecticLowPowers.lean 2 declarations
- MetaplecticMellinGrowth.lean 2 declarations
- MetaplecticMellinMean.lean 4 declarations
- MetaplecticMellinShift.lean 4 declarations
- MetaplecticNaturalCutoff.lean 5 declarations
- MetaplecticNegativeEstimate.lean 1 declarations
- MetaplecticNegativeKernel.lean 2 declarations
- MetaplecticNegativeShort.lean 2 declarations
- MetaplecticNegativeSubpower.lean 1 declarations
- MetaplecticNegativeTail.lean 1 declarations
- MetaplecticNormDyads.lean 11 declarations
- MetaplecticPartialSums.lean 8 declarations
- MetaplecticPoleContour.lean 12 declarations
- MetaplecticPoleCutoff.lean 9 declarations
- MetaplecticPrefixAmplitude.lean 6 declarations
- MetaplecticPrefixBound.lean 2 declarations
- MetaplecticPrefixCutoff.lean 3 declarations
- MetaplecticPrefixMass.lean 3 declarations
- MetaplecticPrefixSum.lean 3 declarations
- MetaplecticPrimalFinite.lean 12 declarations
- MetaplecticPrimalShort.lean 2 declarations
- MetaplecticPrimaryCompletion.lean 7 declarations
- MetaplecticPrimaryInverse.lean 7 declarations
- MetaplecticRadialCentered.lean 4 declarations
- MetaplecticRadialDensity.lean 4 declarations
- MetaplecticRadialDyadic.lean 1 declarations
- MetaplecticRadialEulerTail.lean 2 declarations
- MetaplecticRadialLattice.lean 4 declarations
- MetaplecticRadialLowPower.lean 1 declarations
- MetaplecticRadialModel.lean 4 declarations
- MetaplecticRadialPowers.lean 2 declarations
- MetaplecticRadialResidue.lean 3 declarations
- MetaplecticRadialSelected.lean 1 declarations
- MetaplecticRegularGluing.lean 4 declarations
- MetaplecticRegularGrowth.lean 7 declarations
- MetaplecticRegularMellin.lean 7 declarations
- MetaplecticRetainedContinuity.lean 4 declarations
- MetaplecticRetainedCritical.lean 5 declarations
- MetaplecticRetainedEstimate.lean 3 declarations
- MetaplecticRetainedKernel.lean 1 declarations
- MetaplecticRetainedMean.lean 2 declarations
- MetaplecticRetainedPowers.lean 3 declarations
- MetaplecticRetainedSubpower.lean 1 declarations
- MetaplecticRetainedSupport.lean 7 declarations
- MetaplecticScaleMellin.lean 1 declarations
- MetaplecticScaledAmplitude.lean 4 declarations
- MetaplecticSelectedOuter.lean 2 declarations
- MetaplecticShiftedVoronoi.lean 4 declarations
- MetaplecticShortInverse.lean 3 declarations
- MetaplecticShortLogInverse.lean 4 declarations
- MetaplecticShortModelLow.lean 2 declarations
- MetaplecticShortOuter.lean 2 declarations
- MetaplecticShortResidue.lean 2 declarations
- MetaplecticShortScale.lean 2 declarations
- MetaplecticSmallLow.lean 1 declarations
- MetaplecticSmoothBilinear.lean 4 declarations
- MetaplecticSmoothScale.lean 3 declarations
- MetaplecticSquarefreeBilinear.lean 2 declarations
- MetaplecticSquarefreeRadial.lean 3 declarations
- MetaplecticStripGrowth.lean 6 declarations
- MetaplecticSupportedMean.lean 1 declarations
- MetaplecticSupportedSum.lean 2 declarations
- MetaplecticTailCoefficient.lean 9 declarations
- MetaplecticTailCounting.lean 2 declarations
- MetaplecticTailDyad.lean 1 declarations
- MetaplecticTailLevel.lean 5 declarations
- MetaplecticTailScale.lean 3 declarations
- MetaplecticTailSieve.lean 1 declarations
- MetaplecticTailTruncation.lean 3 declarations
- MetaplecticTotient.lean 5 declarations
- MetaplecticTransformBounds.lean 7 declarations
- MetaplecticTransformContour.lean 7 declarations
- MetaplecticTransformDecay.lean 3 declarations
- MetaplecticTrivialSum.lean 1 declarations
- MetaplecticTwistedGrowth.lean 2 declarations
- MetaplecticTwistedTail.lean 1 declarations
- MetaplecticTwistedTransform.lean 6 declarations
- MetaplecticUniformAngular.lean 3 declarations
- MetaplecticUniformInverse.lean 1 declarations
- MetaplecticUniformLong.lean 2 declarations
- MetaplecticUniformNegativeLong.lean 2 declarations
- MetaplecticUniformRadialInverse.lean 1 declarations
- MetaplecticUniformRetained.lean 2 declarations
- MetaplecticUniformShort.lean 2 declarations
- MetaplecticUniformTail.lean 1 declarations
- MetaplecticUniformTruncation.lean 2 declarations
- MetaplecticUniformWeights.lean 5 declarations
- MetaplecticVoronoi.lean 27 declarations
- MetaplecticVoronoiStrip.lean 3 declarations
- MetaplecticWeightedBilinear.lean 2 declarations
- MetaplecticWeightedContinuation.lean 3 declarations