`OAI/NumberTheory/CubicMoment/Angular/`

809 declarations, 0 contain sorry, 0 declared as axioms; 376 files

Files

AngularAlgebra.lean 16 declarations
AngularArithmeticTwist.lean 7 declarations
AngularBalancedFullRows.lean 2 declarations
AngularBalancedFullSmoothFactor.lean 1 declarations
AngularBalancedLogSmallTwist.lean 1 declarations
AngularBalancedScaledStructuredMoment.lean 1 declarations
AngularBalancedSmallPartTransfer.lean 2 declarations
AngularBalancedSmallTwistCutoff.lean 1 declarations
AngularBalancedSmallTwistPower.lean 1 declarations
AngularBalancedSmoothNeighborhood.lean 1 declarations
AngularBalancedTruncatedNeighborhood.lean 1 declarations
AngularBalancedUniformCoordinateNeighborhood.lean 1 declarations
AngularBalancedUnsplitNeighborhood.lean 1 declarations
AngularBalancedUnweightedStructuredMoment.lean 1 declarations
AngularBalancedWeightedNeighborhood.lean 1 declarations
AngularCenteredPrimeBilinear.lean 1 declarations
AngularCommonBalancedStructuredMoment.lean 1 declarations
AngularCommonCoordinateExponents.lean 2 declarations
AngularCommonFirstSmallSecondConductor.lean 1 declarations
AngularCommonFirstStructuredMoment.lean 1 declarations
AngularCommonNormalizedExponents.lean 2 declarations
AngularCommonPrimeIndicatorExponents.lean 2 declarations
AngularCommonSquarefreePrimeExponents.lean 2 declarations
AngularComplexWeightedConvolution.lean 1 declarations
AngularConductorPhase.lean 5 declarations
AngularCoordinatePrimeMoment.lean 1 declarations
AngularCoordinateWeightedTuple.lean 4 declarations
AngularCoprimeLattice.lean 6 declarations
AngularCoprimeNoncubeIntegral.lean 1 declarations
AngularCorrectedDispersionTheorem.lean 1 declarations
AngularCorrectedPrimeBilinear.lean 1 declarations
AngularCubeLogSaving.lean 1 declarations
AngularCubeMassLogSaving.lean 1 declarations
AngularCubeModelLogSaving.lean 1 declarations
AngularDispersionAbsoluteModel.lean 1 declarations
AngularDispersionModelEnergy.lean 1 declarations
AngularDispersionModelNorm.lean 1 declarations
AngularDistinguishedRowsSaving.lean 1 declarations
AngularDivisorFullModel.lean 1 declarations
AngularDivisorGramAsymptotic.lean 1 declarations
AngularDivisorHighSaving.lean 1 declarations
AngularDivisorLogEnvelope.lean 1 declarations
AngularDivisorLogTail.lean 1 declarations
AngularDivisorModelAsymptotic.lean 1 declarations
AngularDivisorNoncubeAnnulus.lean 1 declarations
AngularDivisorNoncubeDyadic.lean 1 declarations
AngularDivisorNoncubeTotal.lean 1 declarations
AngularDominantBalancedFactor.lean 1 declarations
AngularDominantFirstFactor.lean 1 declarations
AngularDominantNeighborhood.lean 2 declarations
AngularDualContour.lean 7 declarations
AngularDualMoment.lean 5 declarations
AngularDualTail.lean 4 declarations
AngularDyadicMoment.lean 3 declarations
AngularDyadicNoncubeMoment.lean 1 declarations
AngularExceptionalResidualMoment.lean 1 declarations
AngularExceptionalStructuredMoment.lean 1 declarations
AngularExcludedKummerLogSaving.lean 1 declarations
AngularFirstMoment.lean 10 declarations
AngularFirstScaledStructuredMoment.lean 1 declarations
AngularFirstSmoothNeighborhood.lean 1 declarations
AngularFirstTruncatedNeighborhood.lean 1 declarations
AngularFirstUniformCoordinateNeighborhood.lean 1 declarations
AngularFirstUnsplitNeighborhood.lean 1 declarations
AngularFirstUnweightedStructuredMoment.lean 1 declarations
AngularFirstWeightedNeighborhood.lean 1 declarations
AngularFullExceptionalMoment.lean 1 declarations
AngularFullKummerLogSaving.lean 1 declarations
AngularFullNoncubeMoment.lean 1 declarations
AngularFullOrdinaryMoment.lean 1 declarations
AngularFullPrimeConvolution.lean 4 declarations
AngularFullPrimeModelOverlap.lean 1 declarations
AngularFullSmoothFactor.lean 7 declarations
AngularGamma.lean 2 declarations
AngularGaussTail.lean 1 declarations
AngularGroupedPrimeHeight.lean 1 declarations
AngularHeatFactor.lean 4 declarations
AngularHeatLattice.lean 7 declarations
AngularHeatNormalization.lean 3 declarations
AngularHeatPolynomial.lean 3 declarations
AngularHeckeCharacter.lean 33 declarations
AngularHeckeFromFourier.lean 1 declarations
AngularHeckeFromHeat.lean 1 declarations
AngularHeckeGrowth.lean 6 declarations
AngularHeightAllFrequencyMass.lean 1 declarations
AngularHeightAllFrequencyMellin.lean 1 declarations
AngularHeightBilinearScale.lean 1 declarations
AngularHeightCoefficient.lean 10 declarations
AngularHeightCoprimeDispersion.lean 1 declarations
AngularHeightCoprimeIntegral.lean 1 declarations
AngularHeightDivisorBounds.lean 10 declarations
AngularHeightFullVariance.lean 1 declarations
AngularHeightNoStopBound.lean 1 declarations
AngularHeightNoncubeMass.lean 1 declarations
AngularHeightPoissonAnnulus.lean 1 declarations
AngularHeightPoissonDyadic.lean 1 declarations
AngularHeightPoissonTail.lean 3 declarations
AngularHeightPoissonTotal.lean 1 declarations
AngularHeightRadialForm.lean 1 declarations
AngularHeightSignedBound.lean 1 declarations
AngularHeightSignedMellin.lean 2 declarations
AngularKummerAlgebra.lean 3 declarations
AngularKummerLogSaving.lean 1 declarations
AngularKummerPrimeFactorization.lean 2 declarations
AngularKummerPrimeSum.lean 3 declarations
AngularKummerWeightVariation.lean 3 declarations
AngularLargeConductorMoment.lean 1 declarations
AngularLargeCoreBlockMoment.lean 1 declarations
AngularLargeCoreMellinIntegral.lean 1 declarations
AngularLargeCorePolynomialHeight.lean 1 declarations
AngularLargeTupleExceptionalHigh.lean 6 declarations
AngularLargeTupleFlatHigh.lean 1 declarations
AngularLargeTupleFlatSum.lean 2 declarations
AngularLargeTupleGroupKernel.lean 1 declarations
AngularLargeTupleHighSum.lean 3 declarations
AngularLargeTupleNearFlatKernel.lean 1 declarations
AngularLargeTupleNonflatHigh.lean 1 declarations
AngularLargeTupleOrdinaryHigh.lean 1 declarations
AngularLargeTupleOrdinarySum.lean 2 declarations
AngularLargeTupleRestrictedSmoothed.lean 1 declarations
AngularLargeTupleSelectedFlat.lean 2 declarations
AngularLargeTupleTripleKernel.lean 1 declarations
AngularLargeTupleTripleTransition.lean 1 declarations
AngularLatticeCoset.lean 2 declarations
AngularLatticeModel.lean 5 declarations
AngularLatticeProfile.lean 11 declarations
AngularLogBalancedSmallParts.lean 1 declarations
AngularLogCutoff.lean 13 declarations
AngularLogSmallPartTransfer.lean 1 declarations
AngularLogSmallTwist.lean 2 declarations
AngularLogarithmicBalancedStructuredMoment.lean 1 declarations
AngularLogarithmicFirstStructuredMoment.lean 1 declarations
AngularLogarithmicLattice.lean 2 declarations
AngularLongDistinguishedContext.lean 1 declarations
AngularLongDistinguishedInterval.lean 1 declarations
AngularLongDistinguishedPrime.lean 1 declarations
AngularLongDistinguishedSaving.lean 2 declarations
AngularLongPrimeBin.lean 1 declarations
AngularLongPrimeBox.lean 1 declarations
AngularLongPrimeContext.lean 1 declarations
AngularLongPrimeCutoff.lean 2 declarations
AngularLongPrimeMoebius.lean 1 declarations
AngularLongPrimeSW.lean 2 declarations
AngularLongPrimeSaving.lean 1 declarations
AngularLowCoreMellinIntegral.lean 1 declarations
AngularLowCoreMonotone.lean 1 declarations
AngularLowNoncubeMass.lean 1 declarations
AngularMixedModelLogSaving.lean 1 declarations
AngularModel.lean 19 declarations
AngularModelOuter.lean 4 declarations
AngularNoStopNegligible.lean 3 declarations
AngularNoncubeMellinIntegral.lean 1 declarations
AngularNoncubePoissonAnnulus.lean 1 declarations
AngularNoncubePoissonDyadic.lean 1 declarations
AngularNoncubePoissonTotal.lean 1 declarations
AngularNoncubeRadialForm.lean 1 declarations
AngularNoncubeReflectedIntegral.lean 1 declarations
AngularNormalizedCoordinateMoments.lean 3 declarations
AngularNormalizedCoordinateTuple.lean 2 declarations
AngularNumeratorCharacter.lean 7 declarations
AngularNumeratorConductor.lean 2 declarations
AngularOrdinaryStoppedTail.lean 6 declarations
AngularOrdinaryTail.lean 5 declarations
AngularPolynomialHeightCoreBlock.lean 1 declarations
AngularPowerWeights.lean 2 declarations
AngularPrimaryLattice.lean 6 declarations
AngularPrimeCoordinateCollection.lean 9 declarations
AngularPrimeCoordinateErrors.lean 2 declarations
AngularPrimeEulerExclusion.lean 4 declarations
AngularPrimeExplicit.lean 2 declarations
AngularPrimeFromPrimitive.lean 1 declarations
AngularPrimeGroupTailProductEnvelope.lean 1 declarations
AngularPrimeIndicatorMomentTransfer.lean 1 declarations
AngularPrimeInputsProof.lean 2 declarations
AngularPrimeMoebiusExtraction.lean 2 declarations
AngularPrimeMomentCoefficient.lean 3 declarations
AngularPrimeProductBilinear.lean 1 declarations
AngularPrimeProductCentered.lean 4 declarations
AngularPrimeProductCenteredTail.lean 1 declarations
AngularPrimeProductMellinTail.lean 1 declarations
AngularPrimeProductModelMass.lean 2 declarations
AngularPrimeProductPolynomialBounds.lean 3 declarations
AngularPrimeProductSmoothedBilinear.lean 1 declarations
AngularPrimeTailHeckeMean.lean 1 declarations
AngularPrimeTailHeckeTail.lean 1 declarations
AngularPrimeTailHighProduct.lean 1 declarations
AngularPrimeTailLowProduct.lean 1 declarations
AngularPrimeTailProductMean.lean 1 declarations
AngularPrimeTailReduction.lean 1 declarations
AngularPrimeTransitionBilinear.lean 1 declarations
AngularPrimeTransitionDensity.lean 1 declarations
AngularPrimeTransitionHeight.lean 1 declarations
AngularPrimeTupleSize.lean 3 declarations
AngularPrimitiveDualMoments.lean 4 declarations
AngularPrimitiveRetainedMoment.lean 2 declarations
AngularRealScaleLargeMoment.lean 1 declarations
AngularResidueLift.lean 9 declarations
AngularRestrictedNoStopParameters.lean 2 declarations
AngularRestrictedNoStopWindow.lean 1 declarations
AngularRoughKummerLowHeight.lean 1 declarations
AngularRoughNoncubeLowHeight.lean 1 declarations
AngularScaleFirstCentralNegligible.lean 1 declarations
AngularScaleFirstCentralReduction.lean 1 declarations
AngularScaleFirstEarlyNegligible.lean 1 declarations
AngularScaleFirstHighSum.lean 3 declarations
AngularScaleFirstLateNegligible.lean 1 declarations
AngularScaleFirstMiddleBound.lean 1 declarations
AngularScaleFirstMiddleSum.lean 2 declarations
AngularScaleFirstNoStopTail.lean 1 declarations
AngularScaleFirstReduction.lean 3 declarations
AngularScaleFirstStoppedAggregation.lean 2 declarations
AngularScaleFirstStoppedDyads.lean 5 declarations
AngularScaleFirstStoppedEarly.lean 1 declarations
AngularScaleFirstStoppedGeometry.lean 2 declarations
AngularScaleFirstStoppedLate.lean 1 declarations
AngularScaleFirstStoppedReduction.lean 1 declarations
AngularScaleFirstStoppedTransport.lean 1 declarations
AngularScaleFirstStopping.lean 2 declarations
AngularSemiprimeLowKernel.lean 1 declarations
AngularSemiprimeNegligible.lean 1 declarations
AngularSemiprimeSmoothed.lean 4 declarations
AngularShortOuterWindow.lean 1 declarations
AngularShortProductSize.lean 1 declarations
AngularShortTupleMellin.lean 3 declarations
AngularShortTuplePartition.lean 5 declarations
AngularShortTupleScales.lean 2 declarations
AngularShortUnsplitTuple.lean 1 declarations
AngularSievedFullModel.lean 1 declarations
AngularSievedSquarefreeModel.lean 1 declarations
AngularSignedNoncubeIntegral.lean 1 declarations
AngularSinglePrimeTransitionInput.lean 1 declarations
AngularSmallConductorLogSaving.lean 1 declarations
AngularSmallCoreBlockMoment.lean 1 declarations
AngularSmallPairParts.lean 1 declarations
AngularSmallPartCharacter.lean 3 declarations
AngularSmallPartTransfer.lean 4 declarations
AngularSmallTwistCutoff.lean 1 declarations
AngularSmallTwistPower.lean 1 declarations
AngularSmallTwistSmoothMoment.lean 2 declarations
AngularSmoothApproximation.lean 3 declarations
AngularSmoothShortContinuity.lean 1 declarations
AngularSmoothShortFamily.lean 5 declarations
AngularSmoothShortMoments.lean 4 declarations
AngularSmoothShortNeighborhoods.lean 2 declarations
AngularSquareCompletion.lean 3 declarations
AngularSquarefreeCoordinateErrors.lean 2 declarations
AngularSquarefreeIdentity.lean 8 declarations
AngularSquarefreeLattice.lean 6 declarations
AngularSquarefreeMomentTransfer.lean 1 declarations
AngularSquarefreeTwists.lean 3 declarations
AngularStoppedActualCommon.lean 1 declarations
AngularStoppedAggregation.lean 5 declarations
AngularStoppedAllTuples.lean 1 declarations
AngularStoppedCenteredBilinear.lean 1 declarations
AngularStoppedCharacterRows.lean 6 declarations
AngularStoppedCoefficient.lean 3 declarations
AngularStoppedCoreBlocks.lean 1 declarations
AngularStoppedCorrectedDispersion.lean 1 declarations
AngularStoppedCubeError.lean 1 declarations
AngularStoppedCubeMass.lean 1 declarations
AngularStoppedCubeModel.lean 1 declarations
AngularStoppedCubeRoughness.lean 1 declarations
AngularStoppedCubeSW.lean 1 declarations
AngularStoppedDistinguishedFull.lean 2 declarations
AngularStoppedDistinguishedIdentity.lean 1 declarations
AngularStoppedDistinguishedLogSaving.lean 1 declarations
AngularStoppedDistinguishedRow.lean 1 declarations
AngularStoppedDistinguishedRows.lean 2 declarations
AngularStoppedDistinguishedSaving.lean 1 declarations
AngularStoppedDivisorAnnulus.lean 1 declarations
AngularStoppedDivisorCube.lean 2 declarations
AngularStoppedDivisorDyadic.lean 1 declarations
AngularStoppedDivisorModel.lean 1 declarations
AngularStoppedDivisorPartition.lean 2 declarations
AngularStoppedDivisorRows.lean 3 declarations
AngularStoppedDivisorTotal.lean 1 declarations
AngularStoppedEarlyDivisorMass.lean 1 declarations
AngularStoppedEmptyTuple.lean 1 declarations
AngularStoppedFilteredCore.lean 2 declarations
AngularStoppedFullModel.lean 1 declarations
AngularStoppedHeightFactors.lean 1 declarations
AngularStoppedLargeDivisorMass.lean 1 declarations
AngularStoppedLargeDivisorPower.lean 1 declarations
AngularStoppedLargeDivisorRows.lean 1 declarations
AngularStoppedLongBinSaving.lean 3 declarations
AngularStoppedLowCoreMass.lean 1 declarations
AngularStoppedMellinIntegral.lean 1 declarations
AngularStoppedMellinRows.lean 3 declarations
AngularStoppedMixedLogSaving.lean 1 declarations
AngularStoppedMixedModel.lean 1 declarations
AngularStoppedMixedTypeI.lean 1 declarations
AngularStoppedModelNorm.lean 1 declarations
AngularStoppedModelOverlap.lean 1 declarations
AngularStoppedNoncubeMass.lean 1 declarations
AngularStoppedNormMellin.lean 1 declarations
AngularStoppedOrdinaryLowSaving.lean 1 declarations
AngularStoppedOuterCoefficient.lean 5 declarations
AngularStoppedPrimeBox.lean 1 declarations
AngularStoppedPrimeFactorization.lean 2 declarations
AngularStoppedProductLogSaving.lean 1 declarations
AngularStoppedProductLowSaving.lean 1 declarations
AngularStoppedProductModel.lean 1 declarations
AngularStoppedProductTransfer.lean 1 declarations
AngularStoppedRadialForm.lean 1 declarations
AngularStoppedReflectedMellin.lean 1 declarations
AngularStoppedRoughDivisorLog.lean 1 declarations
AngularStoppedRoughDivisorMass.lean 1 declarations
AngularStoppedSelectedBeta.lean 1 declarations
AngularStoppedSelectedCollection.lean 3 declarations
AngularStoppedSelectedDistinguished.lean 1 declarations
AngularStoppedSelectedLogSaving.lean 1 declarations
AngularStoppedSelectedMoment.lean 2 declarations
AngularStoppedSelectedRow.lean 2 declarations
AngularStoppedSequenceRows.lean 2 declarations
AngularStoppedSequenceSW.lean 1 declarations
AngularStoppedShortBinSaving.lean 1 declarations
AngularStoppedSievedModel.lean 1 declarations
AngularStoppedSmallDivisorMass.lean 1 declarations
AngularStoppedSquarefreeModel.lean 1 declarations
AngularStoppedTailBound.lean 1 declarations
AngularStoppedTailTwist.lean 1 declarations
AngularStructuredFrequencyPolynomial.lean 3 declarations
AngularStructuredPartition.lean 5 declarations
AngularStructuredResidualFrequencies.lean 2 declarations
AngularStructuredSupportBounds.lean 1 declarations
AngularStructuredWeightScaling.lean 3 declarations
AngularTailDecompositionEnvelope.lean 1 declarations
AngularTailHighDecomposition.lean 4 declarations
AngularTailHighOrdinaryNegligible.lean 3 declarations
AngularTailHighUpperNegligible.lean 3 declarations
AngularTailPrimeHeckeGroup.lean 1 declarations
AngularTailPrimeHeckeWindow.lean 1 declarations
AngularTailPrimeHighGroup.lean 1 declarations
AngularTailPrimeLowGroup.lean 1 declarations
AngularTailPrimeMiddleGroup.lean 1 declarations
AngularTailPrimeOrdinaryBounds.lean 1 declarations
AngularTailPrimeOrdinaryTuple.lean 2 declarations
AngularTailPrimeRegroup.lean 1 declarations
AngularTailPrimeTailGeometry.lean 3 declarations
AngularTailPrimeUpperGroupBound.lean 1 declarations
AngularTailPrimeUpperTuple.lean 3 declarations
AngularTripleTransitionBilinear.lean 1 declarations
AngularTripleTransitionCentered.lean 1 declarations
AngularTripleTransitionHeight.lean 1 declarations
AngularTripleTransitionSmoothed.lean 1 declarations
AngularTruncatedDual.lean 4 declarations
AngularTwistedConvolutionNeighborhood.lean 2 declarations
AngularTwistedDualMoments.lean 1 declarations
AngularTwistedEuler.lean 2 declarations
AngularTwistedIdealMatch.lean 2 declarations
AngularTwistedPrimeExpansion.lean 3 declarations
AngularTwistedPrimeNeighborhood.lean 2 declarations
AngularTwistedPrimitive.lean 1 declarations
AngularTwistedPrimitiveFamily.lean 2 declarations
AngularTwistedRetainedMoment.lean 1 declarations
AngularTwistedShortProducts.lean 3 declarations
AngularTwistedSmoothBound.lean 1 declarations
AngularTwistedSmoothMoment.lean 1 declarations
AngularTypeILow.lean 2 declarations
AngularTypeIMixedFull.lean 1 declarations
AngularTypeIMixedLogSaving.lean 1 declarations
AngularTypeIMixedPrime.lean 1 declarations
AngularTypeIProductWindow.lean 1 declarations
AngularUniformHighStoppedTail.lean 1 declarations
AngularUniformLattice.lean 3 declarations
AngularUniformPoisson.lean 3 declarations
AngularUpperLowTail.lean 4 declarations
AngularUpperLowTailUniform.lean 5 declarations
AngularUpperNoStopNegligible.lean 3 declarations
AngularUpperNoStopRow.lean 1 declarations
AngularUpperStoppedSuffix.lean 4 declarations
AngularUpperTailAggregation.lean 3 declarations
AngularUpperTailEnvelope.lean 1 declarations
AngularWeightOperator.lean 14 declarations
AngularWeightedTupleMellin.lean 1 declarations
AngularWideLogDenominator.lean 2 declarations