`OAI/NumberTheory/CubicMoment/Theta/`

6587 declarations, 0 contain sorry, 0 declared as axioms; 1476 files

Files

CubicThetaActualCuspCoefficients.lean 9 declarations
CubicThetaActualGaussTails.lean 1 declarations
CubicThetaActualProjection.lean 13 declarations
CubicThetaAdaptedCusp.lean 7 declarations
CubicThetaAdaptedMultiplier.lean 6 declarations
CubicThetaAdditiveMellin.lean 6 declarations
CubicThetaAllGridEquation.lean 2 declarations
CubicThetaAllTypeILow.lean 1 declarations
CubicThetaAmplitudeTail.lean 3 declarations
CubicThetaAngularAdditiveMellin.lean 2 declarations
CubicThetaAngularCompletedBounds.lean 1 declarations
CubicThetaAngularContinuity.lean 2 declarations
CubicThetaAngularContour.lean 1 declarations
CubicThetaAngularConvergence.lean 4 declarations
CubicThetaAngularDirichletContinuation.lean 3 declarations
CubicThetaAngularExponential.lean 7 declarations
CubicThetaAngularFiniteOrder.lean 1 declarations
CubicThetaAngularFrequency.lean 7 declarations
CubicThetaAngularFunctionalEquation.lean 7 declarations
CubicThetaAngularGammaEquation.lean 2 declarations
CubicThetaAngularLeftBound.lean 1 declarations
CubicThetaAngularMellin.lean 2 declarations
CubicThetaAngularOuter.lean 1 declarations
CubicThetaAngularPolynomialStrip.lean 1 declarations
CubicThetaAngularPowers.lean 6 declarations
CubicThetaAngularUpperMellin.lean 4 declarations
CubicThetaAnnularL2.lean 7 declarations
CubicThetaAnnularSeries.lean 13 declarations
CubicThetaArithmetic.lean 17 declarations
CubicThetaArithmeticAxisRegularity.lean 4 declarations
CubicThetaArithmeticChartWeak.lean 3 declarations
CubicThetaArithmeticCriticalImage.lean 2 declarations
CubicThetaArithmeticCubeScaling.lean 4 declarations
CubicThetaArithmeticCuspEnergy.lean 4 declarations
CubicThetaArithmeticCuspMass.lean 3 declarations
CubicThetaArithmeticDistribution.lean 4 declarations
CubicThetaArithmeticEnergy.lean 8 declarations
CubicThetaArithmeticEnergyGraph.lean 3 declarations
CubicThetaArithmeticEquation.lean 4 declarations
CubicThetaArithmeticGlobalWeak.lean 3 declarations
CubicThetaArithmeticGradientL2.lean 8 declarations
CubicThetaArithmeticGradientMass.lean 5 declarations
CubicThetaArithmeticHorizontalTower.lean 7 declarations
CubicThetaArithmeticL2.lean 6 declarations
CubicThetaArithmeticLocalWeak.lean 1 declarations
CubicThetaArithmeticModelEnergy.lean 5 declarations
CubicThetaArithmeticModelIdentity.lean 1 declarations
CubicThetaArithmeticModelInversion.lean 4 declarations
CubicThetaArithmeticModelL2.lean 5 declarations
CubicThetaArithmeticModelObservation.lean 6 declarations
CubicThetaArithmeticModelSection.lean 5 declarations
CubicThetaArithmeticModelTorus.lean 8 declarations
CubicThetaArithmeticPlane.lean 5 declarations
CubicThetaArithmeticPole.lean 2 declarations
CubicThetaArithmeticPoleIsolation.lean 5 declarations
CubicThetaArithmeticPrimeSupport.lean 2 declarations
CubicThetaArithmeticRemainder.lean 9 declarations
CubicThetaArithmeticResolvent.lean 2 declarations
CubicThetaArithmeticRowSeries.lean 7 declarations
CubicThetaArithmeticSection.lean 3 declarations
CubicThetaArithmeticTorus.lean 6 declarations
CubicThetaArithmeticWeakDefect.lean 4 declarations
CubicThetaAutomorphicSections.lean 8 declarations
CubicThetaAveragedHeat.lean 10 declarations
CubicThetaAveragedVoronoi.lean 3 declarations
CubicThetaAxisDerivativeBalance.lean 4 declarations
CubicThetaAxisDifferentials.lean 7 declarations
CubicThetaAxisLineDerivative.lean 2 declarations
CubicThetaBaseScalarNonzero.lean 1 declarations
CubicThetaBaseScalarNorm.lean 3 declarations
CubicThetaBaseScalarReal.lean 4 declarations
CubicThetaBaseScalarSign.lean 2 declarations
CubicThetaBaseScalarValue.lean 3 declarations
CubicThetaBorelInversion.lean 9 declarations
CubicThetaBorelPullback.lean 1 declarations
CubicThetaBorelRestriction.lean 8 declarations
CubicThetaBorelSection.lean 15 declarations
CubicThetaBorelTransport.lean 16 declarations
CubicThetaBottomRow.lean 6 declarations
CubicThetaBottomRowAction.lean 11 declarations
CubicThetaBoundedScaledMellin.lean 6 declarations
CubicThetaC1ChartNorm.lean 1 declarations
CubicThetaC1Cutoff.lean 3 declarations
CubicThetaC1Division.lean 5 declarations
CubicThetaC1Energy.lean 3 declarations
CubicThetaC1EnergyLinear.lean 4 declarations
CubicThetaC1EnergyNorm.lean 2 declarations
CubicThetaC1EnergySums.lean 6 declarations
CubicThetaC1GradientLinear.lean 2 declarations
CubicThetaC1L2.lean 9 declarations
CubicThetaC1Localization.lean 8 declarations
CubicThetaC1Pairing.lean 7 declarations
CubicThetaC1PairingIntegral.lean 3 declarations
CubicThetaCellFourierSeparation.lean 2 declarations
CubicThetaCenteredLow.lean 3 declarations
CubicThetaCenteredSelectedOuter.lean 1 declarations
CubicThetaCenteredShortInverse.lean 1 declarations
CubicThetaCenteredShortLogInverse.lean 1 declarations
CubicThetaCenteredShortModelLow.lean 1 declarations
CubicThetaCentralAngularCenteredPrimeBilinear.lean 1 declarations
CubicThetaCentralAngularCorrectedDispersionTheorem.lean 1 declarations
CubicThetaCentralAngularCorrectedPrimeBilinear.lean 1 declarations
CubicThetaCentralAngularLargeTupleExceptionalHigh.lean 1 declarations
CubicThetaCentralAngularLargeTupleGroupKernel.lean 1 declarations
CubicThetaCentralAngularLargeTupleHighSum.lean 1 declarations
CubicThetaCentralAngularLargeTupleNearFlatKernel.lean 1 declarations
CubicThetaCentralAngularLargeTupleNonflatHigh.lean 1 declarations
CubicThetaCentralAngularLargeTupleOrdinaryHigh.lean 1 declarations
CubicThetaCentralAngularLargeTupleOrdinarySum.lean 1 declarations
CubicThetaCentralAngularLargeTupleRestrictedSmoothed.lean 1 declarations
CubicThetaCentralAngularPrimeProductBilinear.lean 1 declarations
CubicThetaCentralAngularPrimeProductSmoothedBilinear.lean 1 declarations
CubicThetaCentralAngularRestrictedNoStopParameters.lean 1 declarations
CubicThetaCentralAngularScaleFirstCentralNegligible.lean 1 declarations
CubicThetaCentralAngularScaleFirstCentralReduction.lean 1 declarations
CubicThetaCentralAngularScaleFirstEarlyNegligible.lean 1 declarations
CubicThetaCentralAngularScaleFirstHighSum.lean 1 declarations
CubicThetaCentralAngularScaleFirstMiddleBound.lean 1 declarations
CubicThetaCentralAngularScaleFirstMiddleSum.lean 1 declarations
CubicThetaCentralAngularScaleFirstReduction.lean 3 declarations
CubicThetaCentralAngularScaleFirstStoppedEarly.lean 1 declarations
CubicThetaCentralAngularScaleFirstStoppedReduction.lean 1 declarations
CubicThetaCentralAngularSemiprimeLowKernel.lean 1 declarations
CubicThetaCentralAngularSemiprimeNegligible.lean 1 declarations
CubicThetaCentralAngularSemiprimeSmoothed.lean 1 declarations
CubicThetaCentralAngularStoppedCenteredBilinear.lean 1 declarations
CubicThetaCentralAngularStoppedCorrectedDispersion.lean 1 declarations
CubicThetaCentralAngularStoppedMixedLogSaving.lean 1 declarations
CubicThetaCentralAngularStoppedMixedTypeI.lean 1 declarations
CubicThetaCentralAngularStoppedOrdinaryLowSaving.lean 1 declarations
CubicThetaCentralAngularStoppedProductLogSaving.lean 1 declarations
CubicThetaCentralAngularStoppedProductLowSaving.lean 1 declarations
CubicThetaCentralAngularTypeIMixedFull.lean 1 declarations
CubicThetaCentralAngularTypeIMixedLogSaving.lean 1 declarations
CubicThetaCentralAngularTypeIMixedPrime.lean 1 declarations
CubicThetaCentralCenteredPrimeBilinear.lean 1 declarations
CubicThetaCentralCorrectedDispersionTheorem.lean 1 declarations
CubicThetaCentralCorrectedPrimeBilinear.lean 1 declarations
CubicThetaCentralLargeTupleExceptionalHigh.lean 1 declarations
CubicThetaCentralLargeTupleGroupKernel.lean 1 declarations
CubicThetaCentralLargeTupleHighSum.lean 1 declarations
CubicThetaCentralLargeTupleNearFlatKernel.lean 1 declarations
CubicThetaCentralLargeTupleNonflatHigh.lean 1 declarations
CubicThetaCentralLargeTupleOrdinaryHigh.lean 1 declarations
CubicThetaCentralLargeTupleOrdinarySum.lean 1 declarations
CubicThetaCentralLargeTupleRestrictedSmoothed.lean 1 declarations
CubicThetaCentralPrimeProductBilinear.lean 1 declarations
CubicThetaCentralPrimeProductSmoothedBilinear.lean 1 declarations
CubicThetaCentralRestrictedNoStopCentral.lean 1 declarations
CubicThetaCentralRestrictedNoStopParameters.lean 2 declarations
CubicThetaCentralScaleFirstCentralNegligible.lean 1 declarations
CubicThetaCentralScaleFirstEarlyNegligible.lean 1 declarations
CubicThetaCentralScaleFirstHighSum.lean 1 declarations
CubicThetaCentralScaleFirstMiddleBound.lean 1 declarations
CubicThetaCentralScaleFirstMiddleSum.lean 1 declarations
CubicThetaCentralScaleFirstReduction.lean 3 declarations
CubicThetaCentralScaleFirstStoppedEarly.lean 1 declarations
CubicThetaCentralScaleFirstStoppedReduction.lean 2 declarations
CubicThetaCentralSemiprimeBlockEstimate.lean 1 declarations
CubicThetaCentralSemiprimeLowKernel.lean 1 declarations
CubicThetaCentralSemiprimeNegligible.lean 1 declarations
CubicThetaCentralSemiprimePrimeEstimate.lean 1 declarations
CubicThetaCentralSemiprimeSmoothed.lean 1 declarations
CubicThetaCentralShortOuterLow.lean 1 declarations
CubicThetaCentralSinglePrimeBilinear.lean 1 declarations
CubicThetaCentralStoppedCenteredBilinear.lean 1 declarations
CubicThetaCentralStoppedCorrectedDispersion.lean 1 declarations
CubicThetaCentralStoppedMixedLogSaving.lean 1 declarations
CubicThetaCentralStoppedMixedTypeI.lean 1 declarations
CubicThetaCentralStoppedOrdinaryLowSaving.lean 1 declarations
CubicThetaCentralStoppedProductLogSaving.lean 1 declarations
CubicThetaCentralStoppedProductLowSaving.lean 1 declarations
CubicThetaCentralTypeIAdapters.lean 2 declarations
CubicThetaCentralTypeILowHeightTwist.lean 1 declarations
CubicThetaCentralTypeILowIntegral.lean 1 declarations
CubicThetaCentralTypeIMixedFull.lean 1 declarations
CubicThetaCentralTypeIMixedLogSaving.lean 1 declarations
CubicThetaCentralTypeIMixedPrime.lean 1 declarations
CubicThetaCentralTypeIProductLow.lean 1 declarations
CubicThetaCharacterAverage.lean 4 declarations
CubicThetaChartEnergyDomination.lean 5 declarations
CubicThetaChartRestrictedIntegral.lean 2 declarations
CubicThetaChartSections.lean 4 declarations
CubicThetaChartTransition.lean 4 declarations
CubicThetaCircleActual.lean 9 declarations
CubicThetaCircleExtraction.lean 6 declarations
CubicThetaCircleInversion.lean 6 declarations
CubicThetaCircleLimit.lean 1 declarations
CubicThetaCircleNormalized.lean 2 declarations
CubicThetaCirclePlane.lean 3 declarations
CubicThetaCirclePolynomial.lean 6 declarations
CubicThetaCircleSeries.lean 4 declarations
CubicThetaCircleTaylor.lean 8 declarations
CubicThetaCircleTrace.lean 7 declarations
CubicThetaCircleUniform.lean 1 declarations
CubicThetaCoefficientConjugation.lean 4 declarations
CubicThetaCoefficientEnergy.lean 4 declarations
CubicThetaCoefficientMass.lean 5 declarations
CubicThetaCoefficientMellin.lean 4 declarations
CubicThetaCoefficientPrimaryReduction.lean 3 declarations
CubicThetaCoefficientScalar.lean 3 declarations
CubicThetaCoefficientTailSupport.lean 4 declarations
CubicThetaCommonCoefficientBound.lean 4 declarations
CubicThetaCommonCubeScaling.lean 4 declarations
CubicThetaCommonCuspCoefficient.lean 4 declarations
CubicThetaCommonIndex.lean 7 declarations
CubicThetaCommonSupport.lean 3 declarations
CubicThetaCommonTauBound.lean 4 declarations
CubicThetaCompactBorelRestriction.lean 7 declarations
CubicThetaCompactC1Energy.lean 1 declarations
CubicThetaCompactCoreCover.lean 8 declarations
CubicThetaCompactCuspCutoff.lean 7 declarations
CubicThetaCompactCuspEnergy.lean 3 declarations
CubicThetaCompactCuspSupport.lean 2 declarations
CubicThetaCompactDensityBound.lean 4 declarations
CubicThetaCompactDomination.lean 1 declarations
CubicThetaCompactEnergyBound.lean 1 declarations
CubicThetaCompactEnergyCorrection.lean 6 declarations
CubicThetaCompactExponential.lean 1 declarations
CubicThetaCompactHeight.lean 7 declarations
CubicThetaCompactInCore.lean 1 declarations
CubicThetaCompactIncomingTransform.lean 2 declarations
CubicThetaCompactIntegralRestriction.lean 4 declarations
CubicThetaCompactPerturbation.lean 1 declarations
CubicThetaCompactRowBounds.lean 4 declarations
CubicThetaCompactShiftedFamily.lean 7 declarations
CubicThetaCompactShiftedObservation.lean 4 declarations
CubicThetaCompactTransporters.lean 2 declarations
CubicThetaCompletedLong.lean 2 declarations
CubicThetaCompletedLow.lean 3 declarations
CubicThetaCompletedMean.lean 3 declarations
CubicThetaCompletedShort.lean 5 declarations
CubicThetaComplexDensity.lean 2 declarations
CubicThetaComplexHeight.lean 11 declarations
CubicThetaComplexIntegrability.lean 1 declarations
CubicThetaComplexLocalization.lean 8 declarations
CubicThetaComplexPointMeasure.lean 3 declarations
CubicThetaComplexRadialTest.lean 1 declarations
CubicThetaConjugateCoordinates.lean 8 declarations
CubicThetaConjugateProjection.lean 5 declarations
CubicThetaConstantCharacter.lean 3 declarations
CubicThetaConstantContinuation.lean 9 declarations
CubicThetaConstantCount.lean 7 declarations
CubicThetaConstantDirichlet.lean 7 declarations
CubicThetaConstantModeResidue.lean 4 declarations
CubicThetaConstantSpectral.lean 3 declarations
CubicThetaConstantSummability.lean 1 declarations
CubicThetaConstantSupport.lean 3 declarations
CubicThetaContinuedWeakEquation.lean 4 declarations
CubicThetaContinuity.lean 4 declarations
CubicThetaContinuousFourierSeparation.lean 1 declarations
CubicThetaContractionPairing.lean 2 declarations
CubicThetaCoordinateAxis.lean 6 declarations
CubicThetaCoordinateChartIntegral.lean 1 declarations
CubicThetaCoordinateData.lean 4 declarations
CubicThetaCoordinateEnergyBound.lean 2 declarations
CubicThetaCoordinateEnergyClosure.lean 1 declarations
CubicThetaCoordinateIntegrability.lean 1 declarations
CubicThetaCoordinateIntegral.lean 4 declarations
CubicThetaCoordinateIntegrationByParts.lean 2 declarations
CubicThetaCoordinateJets.lean 8 declarations
CubicThetaCoordinateMass.lean 3 declarations
CubicThetaCoordinateNormBounds.lean 7 declarations
CubicThetaCoordinatePairing.lean 6 declarations
CubicThetaCoordinateProfile.lean 7 declarations
CubicThetaCoordinateRegularity.lean 2 declarations
CubicThetaCoordinateSection.lean 5 declarations
CubicThetaCoordinateSectionNorm.lean 1 declarations
CubicThetaCoordinateSectionPairing.lean 4 declarations
CubicThetaCoordinateSectionSupport.lean 3 declarations
CubicThetaCoprimeShear.lean 1 declarations
CubicThetaCoreArguments.lean 6 declarations
CubicThetaCoreBumpIntegral.lean 7 declarations
CubicThetaCoreBumps.lean 4 declarations
CubicThetaCoreCoefficient.lean 4 declarations
CubicThetaCoreCoordinates.lean 8 declarations
CubicThetaCoreDenominator.lean 7 declarations
CubicThetaCoreDivision.lean 2 declarations
CubicThetaCoreLocalRellich.lean 7 declarations
CubicThetaCoreMassCompact.lean 4 declarations
CubicThetaCoreMassFamily.lean 5 declarations
CubicThetaCorePartition.lean 1 declarations
CubicThetaCoreProfiles.lean 7 declarations
CubicThetaCoreRestriction.lean 8 declarations
CubicThetaCoreSections.lean 6 declarations
CubicThetaCubeCancellation.lean 5 declarations
CubicThetaCubeConstant.lean 2 declarations
CubicThetaCubeCoordinates.lean 11 declarations
CubicThetaCubeRowWeight.lean 3 declarations
CubicThetaCuspCharacter.lean 6 declarations
CubicThetaCuspCoefficients.lean 9 declarations
CubicThetaCuspCoordinateEnergy.lean 6 declarations
CubicThetaCuspCoreEnergy.lean 3 declarations
CubicThetaCuspCutoff.lean 7 declarations
CubicThetaCuspCutoffBounds.lean 3 declarations
CubicThetaCuspCutoffEnergy.lean 2 declarations
CubicThetaCuspCutoffMeasurable.lean 2 declarations
CubicThetaCuspDerivativeIntegral.lean 6 declarations
CubicThetaCuspDisjointness.lean 5 declarations
CubicThetaCuspExhaustion.lean 9 declarations
CubicThetaCuspExhaustionBounds.lean 3 declarations
CubicThetaCuspExteriorMass.lean 2 declarations
CubicThetaCuspForcing.lean 4 declarations
CubicThetaCuspFourierIntegral.lean 3 declarations
CubicThetaCuspFourierNormalization.lean 3 declarations
CubicThetaCuspFourierObservable.lean 7 declarations
CubicThetaCuspFourierSurjective.lean 8 declarations
CubicThetaCuspFourierTransform.lean 11 declarations
CubicThetaCuspGreen.lean 10 declarations
CubicThetaCuspHardy.lean 7 declarations
CubicThetaCuspHeatBound.lean 4 declarations
CubicThetaCuspIntegratedHardy.lean 1 declarations
CubicThetaCuspLatticeWeight.lean 9 declarations
CubicThetaCuspLogSection.lean 5 declarations
CubicThetaCuspMassIntegral.lean 3 declarations
CubicThetaCuspNeighborhoodCover.lean 2 declarations
CubicThetaCuspObservable.lean 5 declarations
CubicThetaCuspPeriodicity.lean 4 declarations
CubicThetaCuspPotential.lean 4 declarations
CubicThetaCuspPrimeSupport.lean 3 declarations
CubicThetaCuspRemainder.lean 8 declarations
CubicThetaCuspRemainderBound.lean 3 declarations
CubicThetaCuspRestriction.lean 5 declarations
CubicThetaCuspRowMajorant.lean 5 declarations
CubicThetaCuspRowTransport.lean 5 declarations
CubicThetaCuspScalarIntegrals.lean 8 declarations
CubicThetaCuspSectionHardy.lean 2 declarations
CubicThetaCuspSeparation.lean 4 declarations
CubicThetaCuspStep.lean 13 declarations
CubicThetaCuspStrip.lean 11 declarations
CubicThetaCuspStripEnergy.lean 6 declarations
CubicThetaCuspStripFubini.lean 1 declarations
CubicThetaCuspStripMeasure.lean 5 declarations
CubicThetaCuspStripReduction.lean 5 declarations
CubicThetaCuspTypes.lean 9 declarations
CubicThetaCuspVerticalEnergy.lean 6 declarations
CubicThetaCuspWindowCore.lean 1 declarations
CubicThetaCutoffEnergy.lean 11 declarations
CubicThetaDensityLocal.lean 5 declarations
CubicThetaDerivativeRemainder.lean 4 declarations
CubicThetaDerivativeTailBounds.lean 4 declarations
CubicThetaDirichletBounds.lean 5 declarations
CubicThetaDirichletIntegral.lean 2 declarations
CubicThetaDualFrequency.lean 6 declarations
CubicThetaDualHeatBounds.lean 5 declarations
CubicThetaDualHeatSummability.lean 2 declarations
CubicThetaDualIndex.lean 4 declarations
CubicThetaDualMellinIntegral.lean 7 declarations
CubicThetaDualPhase.lean 3 declarations
CubicThetaDualScalar.lean 3 declarations
CubicThetaEisenstein.lean 10 declarations
CubicThetaEisensteinBounds.lean 6 declarations
CubicThetaEisensteinConvergence.lean 3 declarations
CubicThetaEisensteinCusp.lean 8 declarations
CubicThetaEisensteinFourierRows.lean 3 declarations
CubicThetaEisensteinHolomorphic.lean 5 declarations
CubicThetaEisensteinResidues.lean 8 declarations
CubicThetaEisensteinSpectral.lean 1 declarations
CubicThetaEisensteinTorus.lean 8 declarations
CubicThetaEisensteinUnfold.lean 7 declarations
CubicThetaEllipticTrace.lean 6 declarations
CubicThetaEndpointRegularity.lean 3 declarations
CubicThetaEnergyCoordinates.lean 2 declarations
CubicThetaEnergyIntegralIdentities.lean 3 declarations
CubicThetaEnergyInverseContinuation.lean 3 declarations
CubicThetaEnergyMellin.lean 7 declarations
CubicThetaEnergyPencilKernel.lean 2 declarations
CubicThetaEnergyPoleValue.lean 4 declarations
CubicThetaEnergyRegularDomain.lean 6 declarations
CubicThetaEnergyRegularizer.lean 5 declarations
CubicThetaEnergyResidue.lean 1 declarations
CubicThetaEnergyResolventTransport.lean 6 declarations
CubicThetaEnergySimplePole.lean 4 declarations
CubicThetaEuclideanSmoothing.lean 6 declarations
CubicThetaEven.lean 5 declarations
CubicThetaExceptionalAlgebra.lean 5 declarations
CubicThetaExceptionalProjection.lean 6 declarations
CubicThetaExponential.lean 5 declarations
CubicThetaExtendedAutomorphy.lean 4 declarations
CubicThetaExtendedGroup.lean 7 declarations
CubicThetaExtendedMultiplier.lean 9 declarations
CubicThetaExteriorEnergy.lean 1 declarations
CubicThetaExteriorIntegral.lean 2 declarations
CubicThetaFactorUniqueness.lean 1 declarations
CubicThetaFarCoordinateTail.lean 4 declarations
CubicThetaFiniteConductor.lean 3 declarations
CubicThetaFiniteCongruenceCover.lean 1 declarations
CubicThetaFiniteCoordinateBox.lean 10 declarations
CubicThetaFiniteCover.lean 14 declarations
CubicThetaFiniteCoverIntegral.lean 3 declarations
CubicThetaFiniteCuspEnergy.lean 3 declarations
CubicThetaFiniteCuspRestriction.lean 7 declarations
CubicThetaFiniteCusps.lean 2 declarations
CubicThetaFiniteEnergyClosure.lean 1 declarations
CubicThetaFiniteEnergyPairing.lean 2 declarations
CubicThetaFiniteEnergySections.lean 9 declarations
CubicThetaFiniteEnergySum.lean 3 declarations
CubicThetaFiniteExponential.lean 37 declarations
CubicThetaFiniteFourierInverse.lean 7 declarations
CubicThetaFiniteFourierParseval.lean 7 declarations
CubicThetaFiniteInflation.lean 5 declarations
CubicThetaFiniteKloostermanIntertwiner.lean 6 declarations
CubicThetaFinitePoleInverse.lean 3 declarations
CubicThetaFinitePrimaryProjection.lean 7 declarations
CubicThetaFiniteSpectral.lean 4 declarations
CubicThetaFirstPair.lean 4 declarations
CubicThetaForcedCusp.lean 9 declarations
CubicThetaForcedResidue.lean 7 declarations
CubicThetaForcedResolvent.lean 4 declarations
CubicThetaForcingBoundary.lean 2 declarations
CubicThetaForcingCore.lean 4 declarations
CubicThetaForcingL2.lean 3 declarations
CubicThetaForcingProfile.lean 7 declarations
CubicThetaForcingSeries.lean 6 declarations
CubicThetaForcingSmooth.lean 3 declarations
CubicThetaFourierBessel.lean 3 declarations
CubicThetaFourierCRT.lean 1 declarations
CubicThetaFourierCoefficients.lean 3 declarations
CubicThetaFourierConstant.lean 2 declarations
CubicThetaFourierEnergyIntegrable.lean 2 declarations
CubicThetaFourierEnergyLowPole.lean 5 declarations
CubicThetaFourierHeat.lean 6 declarations
CubicThetaFourierMass.lean 6 declarations
CubicThetaFourierMode.lean 7 declarations
CubicThetaFourierNonzero.lean 4 declarations
CubicThetaFourierParity.lean 3 declarations
CubicThetaFourierPoleIsolation.lean 2 declarations
CubicThetaFourierProfileGram.lean 3 declarations
CubicThetaFourierProfileNorm.lean 4 declarations
CubicThetaFourierProfilePairing.lean 6 declarations
CubicThetaFourierProfileSection.lean 5 declarations
CubicThetaFourierProfileSeries.lean 8 declarations
CubicThetaFourierRadial.lean 5 declarations
CubicThetaFourierRadialScaling.lean 4 declarations
CubicThetaFourierRemainder.lean 10 declarations
CubicThetaFourierStripSeed.lean 5 declarations
CubicThetaFourierStripSupport.lean 4 declarations
CubicThetaFourierStripUnfold.lean 2 declarations
CubicThetaFourierTransform.lean 4 declarations
CubicThetaFreeAction.lean 5 declarations
CubicThetaFreeCubeIndex.lean 7 declarations
CubicThetaFreeCubeParts.lean 3 declarations
CubicThetaFreeLocalVoronoi.lean 8 declarations
CubicThetaFrequencyContinuation.lean 8 declarations
CubicThetaFrequencyDirichlet.lean 7 declarations
CubicThetaFrequencyHolomorphic.lean 4 declarations
CubicThetaFrequencyRemovable.lean 2 declarations
CubicThetaFrequencyResidue.lean 3 declarations
CubicThetaFrequencyTwist.lean 2 declarations
CubicThetaFullEisensteinFourier.lean 5 declarations
CubicThetaFullGaussian.lean 8 declarations
CubicThetaFullGaussianBound.lean 2 declarations
CubicThetaFullGaussianLimit.lean 4 declarations
CubicThetaFullGaussianMellin.lean 8 declarations
CubicThetaFullGaussianRemainder.lean 1 declarations
CubicThetaFullLevelRows.lean 8 declarations
CubicThetaFullMassResidue.lean 3 declarations
CubicThetaFullRows.lean 12 declarations
CubicThetaFunction.lean 8 declarations
CubicThetaFunctionEnergyTransport.lean 2 declarations
CubicThetaFundamentalDomain.lean 7 declarations
CubicThetaFundamentalExtension.lean 7 declarations
CubicThetaGaussConjugation.lean 3 declarations
CubicThetaGaussExpansion.lean 3 declarations
CubicThetaGaussFactor.lean 1 declarations
CubicThetaGaussMellin.lean 7 declarations
CubicThetaGaussParity.lean 4 declarations
CubicThetaGaussTail.lean 1 declarations
CubicThetaGaussTwist.lean 2 declarations
CubicThetaGaussianLinearTail.lean 4 declarations
CubicThetaGaussianPowerBound.lean 4 declarations
CubicThetaGaussianTail.lean 5 declarations
CubicThetaGeometricAfter.lean 3 declarations
CubicThetaGeometricNumerics.lean 7 declarations
CubicThetaGlobalAutomorphicRange.lean 3 declarations
CubicThetaGlobalEnergy.lean 13 declarations
CubicThetaGlobalGradient.lean 15 declarations
CubicThetaGlobalGreen.lean 11 declarations
CubicThetaGlobalL2.lean 8 declarations
CubicThetaGlobalLocalRellich.lean 9 declarations
CubicThetaGlobalLocalizationBound.lean 5 declarations
CubicThetaGlobalMeromorphic.lean 3 declarations
CubicThetaGlobalMultiplier.lean 5 declarations
CubicThetaGlobalResolventWeak.lean 4 declarations
CubicThetaGlobalSpectralResolvent.lean 5 declarations
CubicThetaGlobalWeakInverse.lean 4 declarations
CubicThetaGramCubeCoefficient.lean 2 declarations
CubicThetaGramCubeCutoff.lean 2 declarations
CubicThetaGramCubeFilter.lean 3 declarations
CubicThetaGramCubeInflation.lean 2 declarations
CubicThetaGramCubeLowerLayers.lean 5 declarations
CubicThetaGramCubePrimeCorrection.lean 2 declarations
CubicThetaGramCubePrimePart.lean 2 declarations
CubicThetaGramCubeRecurrence.lean 1 declarations
CubicThetaGramCubeResidueBound.lean 2 declarations
CubicThetaGramCubeTermScaling.lean 2 declarations
CubicThetaGramDenominator.lean 8 declarations
CubicThetaGramDenominatorIntegrable.lean 3 declarations
CubicThetaGramDenominatorIntegral.lean 2 declarations
CubicThetaGramIdentityScaling.lean 2 declarations
CubicThetaGramIntegralDecomposition.lean 8 declarations
CubicThetaGramJointKernel.lean 3 declarations
CubicThetaGramKernelCompact.lean 5 declarations
CubicThetaGramKernelIntegralScaling.lean 3 declarations
CubicThetaGramKernelScaling.lean 3 declarations
CubicThetaGramKloosterman.lean 2 declarations
CubicThetaGramKloostermanFourier.lean 4 declarations
CubicThetaGramPrimeMismatch.lean 4 declarations
CubicThetaGramPrimeSplit.lean 4 declarations
CubicThetaGramPrimeSquareFilter.lean 7 declarations
CubicThetaGramResidueBound.lean 4 declarations
CubicThetaGramRowKernel.lean 4 declarations
CubicThetaGramRowPeriodicity.lean 4 declarations
CubicThetaGramRowReindex.lean 5 declarations
CubicThetaGramRowSupport.lean 3 declarations
CubicThetaGramSinglePrime.lean 3 declarations
CubicThetaGreenAlgebra.lean 5 declarations
CubicThetaGridAnalytic.lean 4 declarations
CubicThetaGridDifferentiation.lean 1 declarations
CubicThetaGridEquation.lean 4 declarations
CubicThetaGridJets.lean 5 declarations
CubicThetaGridLocalJets.lean 3 declarations
CubicThetaGridMajorant.lean 5 declarations
CubicThetaHeatMellinBounds.lean 8 declarations
CubicThetaHeatMoments.lean 4 declarations
CubicThetaHeatPowerSum.lean 4 declarations
CubicThetaHeatScaling.lean 3 declarations
CubicThetaHeatSmallHeight.lean 3 declarations
CubicThetaHeatSmallNonzero.lean 2 declarations
CubicThetaHeatStrip.lean 2 declarations
CubicThetaHeightBandCore.lean 1 declarations
CubicThetaHeightDecay.lean 3 declarations
CubicThetaHeightEquation.lean 3 declarations
CubicThetaHeightNoStopBound.lean 1 declarations
CubicThetaHeightReduction.lean 2 declarations
CubicThetaHeightVoronoi.lean 2 declarations
CubicThetaHeightWindowSeparation.lean 1 declarations
CubicThetaHermitianMetric.lean 6 declarations
CubicThetaHighCuspDerivativeBound.lean 2 declarations
CubicThetaHighCuspDifferentiation.lean 4 declarations
CubicThetaHighCuspRows.lean 4 declarations
CubicThetaHighHeatNonzero.lean 3 declarations
CubicThetaHighWindowPairing.lean 8 declarations
CubicThetaHighWindowSeries.lean 10 declarations
CubicThetaHighWindowSmooth.lean 5 declarations
CubicThetaHilbertCompact.lean 1 declarations
CubicThetaHilbertDiagonal.lean 9 declarations
CubicThetaHorizontalAffine.lean 3 declarations
CubicThetaHorizontalCharacterOrthogonality.lean 4 declarations
CubicThetaHorizontalCoefficient.lean 2 declarations
CubicThetaHorizontalCompact.lean 3 declarations
CubicThetaHorizontalCover.lean 5 declarations
CubicThetaHorizontalDilation.lean 3 declarations
CubicThetaHorizontalDomain.lean 8 declarations
CubicThetaHorizontalEnergy.lean 2 declarations
CubicThetaHorizontalFourierAffine.lean 2 declarations
CubicThetaHorizontalFourierAlgebra.lean 4 declarations
CubicThetaHorizontalFourierCharacter.lean 5 declarations
CubicThetaHorizontalFourierIntegrability.lean 2 declarations
CubicThetaHorizontalFourierTranslation.lean 5 declarations
CubicThetaHorizontalFourierVanishing.lean 2 declarations
CubicThetaHorizontalLattice.lean 10 declarations
CubicThetaHorizontalPeriodFourier.lean 1 declarations
CubicThetaHorizontalPeriodMean.lean 1 declarations
CubicThetaHorizontalPeriodization.lean 6 declarations
CubicThetaHorizontalSection.lean 6 declarations
CubicThetaHorizontalSeriesDerivative.lean 2 declarations
CubicThetaHorizontalTermDerivative.lean 4 declarations
CubicThetaHorizontalTower.lean 7 declarations
CubicThetaHorizontalTranslation.lean 3 declarations
CubicThetaHorizontalUnfold.lean 3 declarations
CubicThetaHyperbolicChain.lean 3 declarations
CubicThetaHyperbolicIntegral.lean 2 declarations
CubicThetaHyperbolicMeasure.lean 12 declarations
CubicThetaHyperbolicOperator.lean 5 declarations
CubicThetaImaginaryTaylor.lean 2 declarations
CubicThetaIncomingCompactIntegral.lean 4 declarations
CubicThetaIncomingEquation.lean 3 declarations
CubicThetaIncomingForcing.lean 5 declarations
CubicThetaIncomingLocalFinite.lean 3 declarations
CubicThetaIncomingRowEquation.lean 1 declarations
CubicThetaIncomingRows.lean 9 declarations
CubicThetaIncomingSmooth.lean 4 declarations
CubicThetaIncomingWindow.lean 15 declarations
CubicThetaIntegerBox.lean 8 declarations
CubicThetaIntegerPeriodicity.lean 7 declarations
CubicThetaIntegralQuotient.lean 9 declarations
CubicThetaInverseResidues.lean 7 declarations
CubicThetaInversionCharacter.lean 6 declarations
CubicThetaInversionDifferential.lean 1 declarations
CubicThetaInversionEnergy.lean 7 declarations
CubicThetaInversionEnergyInvolution.lean 8 declarations
CubicThetaInversionFiniteCompletion.lean 6 declarations
CubicThetaInversionFiniteEnergy.lean 8 declarations
CubicThetaInversionGeometry.lean 6 declarations
CubicThetaInversionHorizontalDerivative.lean 1 declarations
CubicThetaInversionInvolutive.lean 1 declarations
CubicThetaInversionL2Bounds.lean 5 declarations
CubicThetaInversionMass.lean 5 declarations
CubicThetaInversionPairing.lean 4 declarations
CubicThetaInversionRestriction.lean 6 declarations
CubicThetaInversionSmooth.lean 6 declarations
CubicThetaInvertedCoefficients.lean 6 declarations
CubicThetaInvertedCusp.lean 8 declarations
CubicThetaInvertedDirichlet.lean 8 declarations
CubicThetaInvertedFiniteFourier.lean 7 declarations
CubicThetaInvertedFourier.lean 6 declarations
CubicThetaInvertedFourierObservable.lean 7 declarations
CubicThetaInvertedFrequencyBounds.lean 7 declarations
CubicThetaInvertedGaussian.lean 3 declarations
CubicThetaInvertedIncoming.lean 5 declarations
CubicThetaInvertedResidue.lean 8 declarations
CubicThetaInvertedRowFourier.lean 5 declarations
CubicThetaInvertedRowMellin.lean 5 declarations
CubicThetaInvertedRows.lean 8 declarations
CubicThetaInvertedTorus.lean 9 declarations
CubicThetaInvertedUnfold.lean 8 declarations
CubicThetaInvertedWindow.lean 6 declarations
CubicThetaInvertedWindowContinuation.lean 3 declarations
CubicThetaJacobian.lean 6 declarations
CubicThetaJointDifferential.lean 2 declarations
CubicThetaJointMajorant.lean 3 declarations
CubicThetaJointRegularity.lean 2 declarations
CubicThetaJointTermDerivative.lean 6 declarations
CubicThetaKernelAnalytic.lean 5 declarations
CubicThetaKernelEquation.lean 6 declarations
CubicThetaKernelFirstBounds.lean 6 declarations
CubicThetaKernelRatios.lean 6 declarations
CubicThetaKernelSecondBounds.lean 5 declarations
CubicThetaKloostermanCRT.lean 4 declarations
CubicThetaKloostermanCRTPhase.lean 3 declarations
CubicThetaKloostermanCubeInflation.lean 4 declarations
CubicThetaKloostermanEnergy.lean 5 declarations
CubicThetaKloostermanExactEnergy.lean 4 declarations
CubicThetaKloostermanFinite.lean 1 declarations
CubicThetaKloostermanFourierGram.lean 4 declarations
CubicThetaKloostermanHermitian.lean 5 declarations
CubicThetaKloostermanIntegral.lean 4 declarations
CubicThetaKloostermanInversion.lean 5 declarations
CubicThetaKloostermanInvolution.lean 8 declarations
CubicThetaKloostermanNormalization.lean 4 declarations
CubicThetaKloostermanOperator.lean 3 declarations
CubicThetaKloostermanPeriodization.lean 3 declarations
CubicThetaKloostermanResidue.lean 5 declarations
CubicThetaKloostermanUnitScale.lean 2 declarations
CubicThetaKloostermanWeight.lean 6 declarations
CubicThetaKloostermanZeroIndices.lean 5 declarations
CubicThetaKubotaAlternative.lean 4 declarations
CubicThetaKubotaCharacter.lean 4 declarations
CubicThetaKubotaConjugation.lean 8 declarations
CubicThetaKubotaInteger.lean 9 declarations
CubicThetaKubotaMultiplication.lean 4 declarations
CubicThetaKubotaProduct.lean 1 declarations
CubicThetaKubotaReal.lean 2 declarations
CubicThetaKubotaSupplement.lean 2 declarations
CubicThetaKubotaValue.lean 5 declarations
CubicThetaL2Cutoff.lean 7 declarations
CubicThetaL2Dominated.lean 1 declarations
CubicThetaLaplaceSum.lean 6 declarations
CubicThetaLevelAngular.lean 1 declarations
CubicThetaLevelAngularCompleted.lean 3 declarations
CubicThetaLevelAngularMellin.lean 5 declarations
CubicThetaLevelAngularReciprocity.lean 5 declarations
CubicThetaLevelBruhat.lean 6 declarations
CubicThetaLevelInverse.lean 4 declarations
CubicThetaLevelMellin.lean 7 declarations
CubicThetaLevelPlane.lean 1 declarations
CubicThetaLevelReciprocity.lean 5 declarations
CubicThetaLevelTransformation.lean 3 declarations
CubicThetaLocalBudget.lean 2 declarations
CubicThetaLocalCubeTerm.lean 5 declarations
CubicThetaLocalEnergyGraph.lean 9 declarations
CubicThetaLocalEnergyJet.lean 7 declarations
CubicThetaLocalEnergyRellich.lean 10 declarations
CubicThetaLocalEnergyResolvent.lean 3 declarations
CubicThetaLocalGreen.lean 4 declarations
CubicThetaLocalLifts.lean 3 declarations
CubicThetaLocalOperator.lean 2 declarations
CubicThetaLocalQuotientMeasure.lean 3 declarations
CubicThetaLocalRellich.lean 5 declarations
CubicThetaLocalRellichValue.lean 4 declarations
CubicThetaLocalVoronoi.lean 3 declarations
CubicThetaLocalizationLinear.lean 8 declarations
CubicThetaLocalizationSobolevBound.lean 4 declarations
CubicThetaLogHeight.lean 4 declarations
CubicThetaLogMeasure.lean 4 declarations
CubicThetaLongWindow.lean 13 declarations
CubicThetaLongWindowKernel.lean 14 declarations
CubicThetaLowerCusp.lean 7 declarations
CubicThetaLowerCuspPositive.lean 4 declarations
CubicThetaMains.lean 4 declarations
CubicThetaMassEuler.lean 4 declarations
CubicThetaMassFactorization.lean 16 declarations
CubicThetaMassPushforward.lean 2 declarations
CubicThetaMassResidue.lean 6 declarations
CubicThetaMellin.lean 3 declarations
CubicThetaMellinPowers.lean 7 declarations
CubicThetaMellinReciprocity.lean 8 declarations
CubicThetaMellinWeights.lean 4 declarations
CubicThetaMeromorphicApply.lean 1 declarations
CubicThetaMeromorphicIdentity.lean 2 declarations
CubicThetaMeromorphicLinear.lean 1 declarations
CubicThetaMetricDerivative.lean 1 declarations
CubicThetaMetricPairing.lean 4 declarations
CubicThetaMetricScale.lean 3 declarations
CubicThetaMobiusAction.lean 6 declarations
CubicThetaMobiusContinuity.lean 4 declarations
CubicThetaMobiusGenerators.lean 5 declarations
CubicThetaMobiusGeometry.lean 8 declarations
CubicThetaMobiusMatrix.lean 5 declarations
CubicThetaMobiusSmooth.lean 4 declarations
CubicThetaModelGlobalL2.lean 3 declarations
CubicThetaModelRankinLimit.lean 5 declarations
CubicThetaNegativeTail.lean 1 declarations
CubicThetaNineCusp.lean 8 declarations
CubicThetaNineDualPhase.lean 5 declarations
CubicThetaNinePhase.lean 5 declarations
CubicThetaNinePhaseSymbol.lean 4 declarations
CubicThetaNoStopNegligible.lean 1 declarations
CubicThetaNonzeroHeat.lean 8 declarations
CubicThetaNonzeroRowCoordinates.lean 3 declarations
CubicThetaNonzeroRowHeat.lean 8 declarations
CubicThetaNonzeroSpectralResidue.lean 5 declarations
CubicThetaNormalizedJets.lean 4 declarations
CubicThetaNormalizedRamified.lean 3 declarations
CubicThetaNormalizedResidueObservation.lean 2 declarations
CubicThetaNormalizedSeries.lean 6 declarations
CubicThetaObservationScaling.lean 4 declarations
CubicThetaOrdinaryTail.lean 1 declarations
CubicThetaPeriodMeasure.lean 6 declarations
CubicThetaPeriodicity.lean 4 declarations
CubicThetaPoincareLinear.lean 1 declarations
CubicThetaPoincareLocalization.lean 1 declarations
CubicThetaPoincarePairing.lean 1 declarations
CubicThetaPoincareSections.lean 7 declarations
CubicThetaPoincareSmooth.lean 4 declarations
CubicThetaPoincareUnfolding.lean 3 declarations
CubicThetaPointC1.lean 10 declarations
CubicThetaPointC1Hecke.lean 7 declarations
CubicThetaPointC1Inversion.lean 2 declarations
CubicThetaPointC1Pairing.lean 4 declarations
CubicThetaPointC1Section.lean 4 declarations
CubicThetaPointC1Trace.lean 4 declarations
CubicThetaPointC1TraceIntegral.lean 3 declarations
CubicThetaPointFrame.lean 6 declarations
CubicThetaPointMeasureLocallyFinite.lean 3 declarations
CubicThetaPointMeasurePositive.lean 1 declarations
CubicThetaPoleRadialScaling.lean 4 declarations
CubicThetaPositiveAveragedHeat.lean 11 declarations
CubicThetaPositiveContraction.lean 1 declarations
CubicThetaPositiveCuspRestriction.lean 8 declarations
CubicThetaPositiveFourierMass.lean 6 declarations
CubicThetaPositiveFourierObservable.lean 5 declarations
CubicThetaPositiveFourierProfile.lean 6 declarations
CubicThetaPositiveFourierScaling.lean 4 declarations
CubicThetaPositiveFourierSmooth.lean 5 declarations
CubicThetaPositiveGramDiagonal.lean 2 declarations
CubicThetaPositiveHeightBand.lean 2 declarations
CubicThetaPositiveHeightSeparation.lean 1 declarations
CubicThetaPositiveInteriorSource.lean 1 declarations
CubicThetaPositiveLocalization.lean 5 declarations
CubicThetaPositiveModelIdentity.lean 1 declarations
CubicThetaPositiveModelL2.lean 5 declarations
CubicThetaPositiveModelObservation.lean 5 declarations
CubicThetaPositiveNormalizedResidue.lean 2 declarations
CubicThetaPositivePoleScaling.lean 4 declarations
CubicThetaPositiveProfileGram.lean 4 declarations
CubicThetaPositiveProfileSeparation.lean 3 declarations
CubicThetaPositiveRadialMellin.lean 4 declarations
CubicThetaPositiveRadialNormalization.lean 3 declarations
CubicThetaPositiveRadialWindow.lean 4 declarations
CubicThetaPositiveResidueObservation.lean 2 declarations
CubicThetaPositiveSourceScaling.lean 3 declarations
CubicThetaPositiveSquareSource.lean 1 declarations
CubicThetaPositiveStarProduct.lean 2 declarations
CubicThetaPositiveStripBound.lean 3 declarations
CubicThetaPositiveStripFourierSeparation.lean 2 declarations
CubicThetaPositiveStripFubini.lean 5 declarations
CubicThetaPositiveStripHorizontalDensity.lean 4 declarations
CubicThetaPositiveStripPairing.lean 4 declarations
CubicThetaPositiveStripRepresentative.lean 7 declarations
CubicThetaPositiveUnfold.lean 1 declarations
CubicThetaPositiveZeroWindow.lean 5 declarations
CubicThetaPrimaryBottom.lean 7 declarations
CubicThetaPrimaryBruhat.lean 3 declarations
CubicThetaPrimaryCoefficients.lean 5 declarations
CubicThetaPrimaryConstant.lean 5 declarations
CubicThetaPrimaryCubes.lean 10 declarations
CubicThetaPrimaryFourierTwist.lean 3 declarations
CubicThetaPrimaryIndex.lean 6 declarations
CubicThetaPrimaryInversion.lean 2 declarations
CubicThetaPrimaryMassEuler.lean 4 declarations
CubicThetaPrimaryNineFourier.lean 3 declarations
CubicThetaPrimaryNineSum.lean 2 declarations
CubicThetaPrimaryObservedCoefficient.lean 4 declarations
CubicThetaPrimaryPeriodicity.lean 4 declarations
CubicThetaPrimaryPowerCoordinates.lean 3 declarations
CubicThetaPrimaryResidue.lean 4 declarations
CubicThetaPrimaryResidueIdentification.lean 5 declarations
CubicThetaPrimaryResidueNine.lean 7 declarations
CubicThetaPrimarySeriesRamification.lean 3 declarations
CubicThetaPrimaryUnitResidue.lean 2 declarations
CubicThetaPrimaryUnitTwist.lean 3 declarations
CubicThetaPrimeAdditiveGauss.lean 6 declarations
CubicThetaPrimeArithmeticResidue.lean 6 declarations
CubicThetaPrimeAtkinAction.lean 7 declarations
CubicThetaPrimeAtkinConjugation.lean 7 declarations
CubicThetaPrimeAtkinEnergyInvolution.lean 8 declarations
CubicThetaPrimeAtkinInvolution.lean 4 declarations
CubicThetaPrimeAtkinMeasure.lean 3 declarations
CubicThetaPrimeAutomorphicL2.lean 6 declarations
CubicThetaPrimeC1Energy.lean 8 declarations
CubicThetaPrimeCharacterAverage.lean 5 declarations
CubicThetaPrimeCharacterNontrivial.lean 2 declarations
CubicThetaPrimeComparison.lean 2 declarations
CubicThetaPrimeConjugate.lean 2 declarations
CubicThetaPrimeConjugation.lean 5 declarations
CubicThetaPrimeConjugationHom.lean 4 declarations
CubicThetaPrimeCosetPermutation.lean 4 declarations
CubicThetaPrimeCoverAtkin.lean 9 declarations
CubicThetaPrimeCoverBorel.lean 16 declarations
CubicThetaPrimeCoverDegree.lean 3 declarations
CubicThetaPrimeCoverDomain.lean 10 declarations
CubicThetaPrimeCoverGroup.lean 14 declarations
CubicThetaPrimeCoverMeasure.lean 3 declarations
CubicThetaPrimeCriticalFactors.lean 5 declarations
CubicThetaPrimeCriticalMatrix.lean 8 declarations
CubicThetaPrimeCubeAtkin.lean 6 declarations
CubicThetaPrimeCubeAtkinIntegral.lean 6 declarations
CubicThetaPrimeCubeAtkinPairing.lean 5 declarations
CubicThetaPrimeCubeBottomMean.lean 3 declarations
CubicThetaPrimeCubeBranchCoordinates.lean 4 declarations
CubicThetaPrimeCubeBranchFourier.lean 8 declarations
CubicThetaPrimeCubeBranchPeriodicity.lean 3 declarations
CubicThetaPrimeCubeChartCover.lean 3 declarations
CubicThetaPrimeCubeChartEquiv.lean 6 declarations
CubicThetaPrimeCubeCompletedAdjoint.lean 5 declarations
CubicThetaPrimeCubeComplexIntegration.lean 3 declarations
CubicThetaPrimeCubeConjugation.lean 4 declarations
CubicThetaPrimeCubeCosets.lean 7 declarations
CubicThetaPrimeCubeCoverDomain.lean 5 declarations
CubicThetaPrimeCubeDegree.lean 5 declarations
CubicThetaPrimeCubeDerivativeAdjoint.lean 2 declarations
CubicThetaPrimeCubeDilationNorm.lean 7 declarations
CubicThetaPrimeCubeDirichlet.lean 2 declarations
CubicThetaPrimeCubeEnergyIntegral.lean 5 declarations
CubicThetaPrimeCubeFiniteAdjoint.lean 3 declarations
CubicThetaPrimeCubeFiniteEnergy.lean 7 declarations
CubicThetaPrimeCubeFirstBranchMean.lean 4 declarations
CubicThetaPrimeCubeFirstCoefficient.lean 3 declarations
CubicThetaPrimeCubeFirstFourier.lean 3 declarations
CubicThetaPrimeCubeFirstPeriodMean.lean 3 declarations
CubicThetaPrimeCubeFirstPeriodization.lean 6 declarations
CubicThetaPrimeCubeFourierKernel.lean 7 declarations
CubicThetaPrimeCubeFourierMode.lean 9 declarations
CubicThetaPrimeCubeFourierNormalization.lean 2 declarations
CubicThetaPrimeCubeFourierOperator.lean 7 declarations
CubicThetaPrimeCubeFourierPairing.lean 2 declarations
CubicThetaPrimeCubeFourierPhase.lean 1 declarations
CubicThetaPrimeCubeGauss.lean 5 declarations
CubicThetaPrimeCubeHeckeEnergy.lean 2 declarations
CubicThetaPrimeCubeHeckeEnergyOperator.lean 6 declarations
CubicThetaPrimeCubeHeckeFormula.lean 9 declarations
CubicThetaPrimeCubeHeckeFourier.lean 2 declarations
CubicThetaPrimeCubeHeckeLinear.lean 4 declarations
CubicThetaPrimeCubeHeckePairing.lean 6 declarations
CubicThetaPrimeCubeHeckeRegularity.lean 5 declarations
CubicThetaPrimeCubeHeightMultiplier.lean 5 declarations
CubicThetaPrimeCubeHighSource.lean 6 declarations
CubicThetaPrimeCubeHorizontalContinuity.lean 5 declarations
CubicThetaPrimeCubeHorizontalMean.lean 3 declarations
CubicThetaPrimeCubeInflation.lean 3 declarations
CubicThetaPrimeCubeInteriorFourier.lean 1 declarations
CubicThetaPrimeCubeInvariantDilation.lean 8 declarations
CubicThetaPrimeCubeLowerChart.lean 1 declarations
CubicThetaPrimeCubeLowerValue.lean 7 declarations
CubicThetaPrimeCubeMassOperator.lean 10 declarations
CubicThetaPrimeCubeNormalizerCosets.lean 4 declarations
CubicThetaPrimeCubeOppositeBranch.lean 3 declarations
CubicThetaPrimeCubeOppositeConjugation.lean 6 declarations
CubicThetaPrimeCubeRadialPairing.lean 4 declarations
CubicThetaPrimeCubeRadialResidue.lean 3 declarations
CubicThetaPrimeCubeReciprocalGeometry.lean 4 declarations
CubicThetaPrimeCubeReciprocalNormalizer.lean 4 declarations
CubicThetaPrimeCubeReductionPhase.lean 3 declarations
CubicThetaPrimeCubeReductionResidue.lean 5 declarations
CubicThetaPrimeCubeReductionRow.lean 7 declarations
CubicThetaPrimeCubeResidueComplement.lean 1 declarations
CubicThetaPrimeCubeResidueEigenvalue.lean 2 declarations
CubicThetaPrimeCubeResiduePeriodicity.lean 1 declarations
CubicThetaPrimeCubeResidueStep.lean 11 declarations
CubicThetaPrimeCubeResidueTestWeight.lean 4 declarations
CubicThetaPrimeCubeRootAction.lean 2 declarations
CubicThetaPrimeCubeRootAutomorphicL2.lean 6 declarations
CubicThetaPrimeCubeRootAutomorphism.lean 4 declarations
CubicThetaPrimeCubeRootAverageIdentity.lean 1 declarations
CubicThetaPrimeCubeRootAverageObservation.lean 2 declarations
CubicThetaPrimeCubeRootBruhat.lean 7 declarations
CubicThetaPrimeCubeRootBruhatL2.lean 5 declarations
CubicThetaPrimeCubeRootBruhatPhase.lean 6 declarations
CubicThetaPrimeCubeRootConjugation.lean 4 declarations
CubicThetaPrimeCubeRootCorrelationFormula.lean 2 declarations
CubicThetaPrimeCubeRootCoverDomain.lean 17 declarations
CubicThetaPrimeCubeRootCriticalSquare.lean 2 declarations
CubicThetaPrimeCubeRootCuspLift.lean 2 declarations
CubicThetaPrimeCubeRootCuspObservation.lean 6 declarations
CubicThetaPrimeCubeRootCuspRestriction.lean 5 declarations
CubicThetaPrimeCubeRootDeepCharacter.lean 4 declarations
CubicThetaPrimeCubeRootDilation.lean 5 declarations
CubicThetaPrimeCubeRootDilationFixed.lean 5 declarations
CubicThetaPrimeCubeRootDilationL2.lean 4 declarations
CubicThetaPrimeCubeRootDilationObservation.lean 4 declarations
CubicThetaPrimeCubeRootDomainMass.lean 3 declarations
CubicThetaPrimeCubeRootFirstIntegral.lean 6 declarations
CubicThetaPrimeCubeRootFourier.lean 6 declarations
CubicThetaPrimeCubeRootFourierNorm.lean 3 declarations
CubicThetaPrimeCubeRootFourierProducts.lean 5 declarations
CubicThetaPrimeCubeRootHeckeCover.lean 14 declarations
CubicThetaPrimeCubeRootHeckeIntegral.lean 4 declarations
CubicThetaPrimeCubeRootHorizontal.lean 5 declarations
CubicThetaPrimeCubeRootL2.lean 6 declarations
CubicThetaPrimeCubeRootL2Algebra.lean 7 declarations
CubicThetaPrimeCubeRootLiftL2.lean 7 declarations
CubicThetaPrimeCubeRootMassTransport.lean 4 declarations
CubicThetaPrimeCubeRootMatrix.lean 7 declarations
CubicThetaPrimeCubeRootNonunitCorrelation.lean 4 declarations
CubicThetaPrimeCubeRootNormBalance.lean 3 declarations
CubicThetaPrimeCubeRootObservationProjection.lean 3 declarations
CubicThetaPrimeCubeRootPowerCharacter.lean 4 declarations
CubicThetaPrimeCubeRootPowerOrthogonal.lean 6 declarations
CubicThetaPrimeCubeRootRamanujan.lean 2 declarations
CubicThetaPrimeCubeRootResidueAverage.lean 3 declarations
CubicThetaPrimeCubeRootResidueOverlap.lean 2 declarations
CubicThetaPrimeCubeRootResidues.lean 5 declarations
CubicThetaPrimeCubeRootSecondIntegral.lean 5 declarations
CubicThetaPrimeCubeRootSections.lean 9 declarations
CubicThetaPrimeCubeRootStripBound.lean 4 declarations
CubicThetaPrimeCubeRootTraceNormalized.lean 3 declarations
CubicThetaPrimeCubeRootTracePairing.lean 3 declarations
CubicThetaPrimeCubeRootTranslation.lean 5 declarations
CubicThetaPrimeCubeRootWeight.lean 4 declarations
CubicThetaPrimeCubeRootWeyl.lean 14 declarations
CubicThetaPrimeCubeRootWeylGlobal.lean 4 declarations
CubicThetaPrimeCubeRootWeylL2.lean 5 declarations
CubicThetaPrimeCubeRootWeylMass.lean 3 declarations
CubicThetaPrimeCubeRootWeylSections.lean 5 declarations
CubicThetaPrimeCubeRows.lean 10 declarations
CubicThetaPrimeCubeSecondBranchCoordinates.lean 2 declarations
CubicThetaPrimeCubeSecondBranchMean.lean 2 declarations
CubicThetaPrimeCubeSecondFourier.lean 4 declarations
CubicThetaPrimeCubeSectionAtkin.lean 3 declarations
CubicThetaPrimeCubeSections.lean 3 declarations
CubicThetaPrimeCubeSelfAdjoint.lean 5 declarations
CubicThetaPrimeCubeSelfAdjointSection.lean 3 declarations
CubicThetaPrimeCubeSheetIntegral.lean 3 declarations
CubicThetaPrimeCubeSquareFourier.lean 4 declarations
CubicThetaPrimeCubeSupport.lean 5 declarations
CubicThetaPrimeCubeTrace.lean 7 declarations
CubicThetaPrimeCubeTraceExpansion.lean 2 declarations
CubicThetaPrimeCubeTraceNorm.lean 5 declarations
CubicThetaPrimeCubeTracePairing.lean 2 declarations
CubicThetaPrimeCubeTransversal.lean 8 declarations
CubicThetaPrimeCubeTriangular.lean 7 declarations
CubicThetaPrimeCubeTriangularCoordinates.lean 3 declarations
CubicThetaPrimeCubeUnitBranch.lean 1 declarations
CubicThetaPrimeCubeUnitMean.lean 4 declarations
CubicThetaPrimeCubeUnitPermutation.lean 5 declarations
CubicThetaPrimeCubeUpperChart.lean 13 declarations
CubicThetaPrimeCubeValuationSum.lean 3 declarations
CubicThetaPrimeCubeWeakEquation.lean 2 declarations
CubicThetaPrimeCubeZeroMode.lean 5 declarations
CubicThetaPrimeDeterminant.lean 6 declarations
CubicThetaPrimeDiagonal.lean 4 declarations
CubicThetaPrimeDilation.lean 6 declarations
CubicThetaPrimeDilationCoordinates.lean 2 declarations
CubicThetaPrimeDilationRows.lean 5 declarations
CubicThetaPrimeDilationTerms.lean 3 declarations
CubicThetaPrimeDilationUnfold.lean 5 declarations
CubicThetaPrimeDirichlet.lean 9 declarations
CubicThetaPrimeDoubleAtkin.lean 5 declarations
CubicThetaPrimeDoubleRootAction.lean 2 declarations
CubicThetaPrimeDoubleRootAutomorphism.lean 4 declarations
CubicThetaPrimeDoubleRootBruhat.lean 7 declarations
CubicThetaPrimeDoubleRootConjugation.lean 6 declarations
CubicThetaPrimeDoubleRootDomain.lean 6 declarations
CubicThetaPrimeDoubleRootGlobal.lean 2 declarations
CubicThetaPrimeDoubleRootMatrix.lean 8 declarations
CubicThetaPrimeDoubleRootOrthogonal.lean 4 declarations
CubicThetaPrimeDoubleRootPairing.lean 3 declarations
CubicThetaPrimeDoubleRootSections.lean 9 declarations
CubicThetaPrimeDoubleRootTranslation.lean 5 declarations
CubicThetaPrimeDoubleRootTranslationIntegral.lean 2 declarations
CubicThetaPrimeDoubleRootWeyl.lean 14 declarations
CubicThetaPrimeDoubleRootWeylSections.lean 5 declarations
CubicThetaPrimeEnergyDomainNorm.lean 4 declarations
CubicThetaPrimeEnergyInvariant.lean 5 declarations
CubicThetaPrimeEnergyRestriction.lean 6 declarations
CubicThetaPrimeEnergySpace.lean 14 declarations
CubicThetaPrimeEnergyValue.lean 8 declarations
CubicThetaPrimeEulerStep.lean 6 declarations
CubicThetaPrimeFiniteEnergy.lean 7 declarations
CubicThetaPrimeFourier.lean 5 declarations
CubicThetaPrimeFourierOrbit.lean 4 declarations
CubicThetaPrimeFreeContinuation.lean 5 declarations
CubicThetaPrimeFreeSystem.lean 8 declarations
CubicThetaPrimeGauss.lean 2 declarations
CubicThetaPrimeGradient.lean 12 declarations
CubicThetaPrimeHeckeContinuation.lean 5 declarations
CubicThetaPrimeHeckeRelation.lean 3 declarations
CubicThetaPrimeIwahori.lean 8 declarations
CubicThetaPrimeKernelNormaliser.lean 4 declarations
CubicThetaPrimeKloostermanInflation.lean 7 declarations
CubicThetaPrimeKloostermanShift.lean 7 declarations
CubicThetaPrimeKloostermanStationary.lean 4 declarations
CubicThetaPrimeL2.lean 11 declarations
CubicThetaPrimeLiftEnergy.lean 4 declarations
CubicThetaPrimeLiftL2.lean 9 declarations
CubicThetaPrimeLiftOrthogonality.lean 2 declarations
CubicThetaPrimeLocalCases.lean 6 declarations
CubicThetaPrimePairing.lean 4 declarations
CubicThetaPrimePairingL2.lean 6 declarations
CubicThetaPrimePoleFactors.lean 3 declarations
CubicThetaPrimePowerFourier.lean 6 declarations
CubicThetaPrimeResidueDefect.lean 8 declarations
CubicThetaPrimeResidueImage.lean 7 declarations
CubicThetaPrimeResidueObservationMap.lean 7 declarations
CubicThetaPrimeResidueObstruction.lean 3 declarations
CubicThetaPrimeResidueTestWeight.lean 5 declarations
CubicThetaPrimeRestrictionL2.lean 2 declarations
CubicThetaPrimeRootAction.lean 2 declarations
CubicThetaPrimeRootAutomorphicL2.lean 6 declarations
CubicThetaPrimeRootAutomorphism.lean 4 declarations
CubicThetaPrimeRootAverage.lean 5 declarations
CubicThetaPrimeRootAverageBound.lean 4 declarations
CubicThetaPrimeRootBruhat.lean 2 declarations
CubicThetaPrimeRootBruhatMass.lean 2 declarations
CubicThetaPrimeRootBruhatMatrix.lean 5 declarations
CubicThetaPrimeRootBruhatOperators.lean 2 declarations
CubicThetaPrimeRootBruhatResidues.lean 5 declarations
CubicThetaPrimeRootCharacter.lean 3 declarations
CubicThetaPrimeRootConjugation.lean 3 declarations
CubicThetaPrimeRootCoverAction.lean 3 declarations
CubicThetaPrimeRootCoverBorel.lean 16 declarations
CubicThetaPrimeRootCoverDegree.lean 4 declarations
CubicThetaPrimeRootCoverDomain.lean 17 declarations
CubicThetaPrimeRootCoverMeasure.lean 3 declarations
CubicThetaPrimeRootCoverTransport.lean 3 declarations
CubicThetaPrimeRootDiagonal.lean 4 declarations
CubicThetaPrimeRootDilationOrthogonal.lean 4 declarations
CubicThetaPrimeRootDilationSection.lean 3 declarations
CubicThetaPrimeRootDilationWeyl.lean 4 declarations
CubicThetaPrimeRootFourierEnergy.lean 2 declarations
CubicThetaPrimeRootFourierL2.lean 7 declarations
CubicThetaPrimeRootFourierL2Bounds.lean 1 declarations
CubicThetaPrimeRootFourierL2Products.lean 2 declarations
CubicThetaPrimeRootFourierMass.lean 2 declarations
CubicThetaPrimeRootFourierOperators.lean 4 declarations
CubicThetaPrimeRootFourierProducts.lean 4 declarations
CubicThetaPrimeRootFourierResolution.lean 1 declarations
CubicThetaPrimeRootHorizontal.lean 4 declarations
CubicThetaPrimeRootIwahoriConjugation.lean 4 declarations
CubicThetaPrimeRootIwahoriDomain.lean 1 declarations
CubicThetaPrimeRootL2.lean 11 declarations
CubicThetaPrimeRootL2Algebra.lean 3 declarations
CubicThetaPrimeRootLiftL2.lean 7 declarations
CubicThetaPrimeRootMatrix.lean 5 declarations
CubicThetaPrimeRootOperators.lean 7 declarations
CubicThetaPrimeRootOrbitOrthogonal.lean 3 declarations
CubicThetaPrimeRootPairing.lean 7 declarations
CubicThetaPrimeRootPairingL2.lean 3 declarations
CubicThetaPrimeRootResidues.lean 5 declarations
CubicThetaPrimeRootRestrictionBound.lean 4 declarations
CubicThetaPrimeRootRestrictionL2.lean 2 declarations
CubicThetaPrimeRootSectionNorm.lean 6 declarations
CubicThetaPrimeRootSections.lean 5 declarations
CubicThetaPrimeRootSquareCharacter.lean 4 declarations
CubicThetaPrimeRootSquareOrthogonal.lean 2 declarations
CubicThetaPrimeRootSubgroup.lean 3 declarations
CubicThetaPrimeRootTranslation.lean 5 declarations
CubicThetaPrimeRootTranslationIntegral.lean 1 declarations
CubicThetaPrimeRootTranslationL2.lean 5 declarations
CubicThetaPrimeRootWeyl.lean 5 declarations
CubicThetaPrimeRootWeylAverage.lean 3 declarations
CubicThetaPrimeRootWeylCover.lean 3 declarations
CubicThetaPrimeRootWeylFixed.lean 6 declarations
CubicThetaPrimeRootWeylFormula.lean 2 declarations
CubicThetaPrimeRootWeylFourier.lean 1 declarations
CubicThetaPrimeRootWeylGauss.lean 7 declarations
CubicThetaPrimeRootWeylInvolution.lean 5 declarations
CubicThetaPrimeRootWeylKernel.lean 2 declarations
CubicThetaPrimeRootWeylL2.lean 2 declarations
CubicThetaPrimeRootWeylMass.lean 1 declarations
CubicThetaPrimeRootWeylMeasure.lean 5 declarations
CubicThetaPrimeRootWeylSections.lean 3 declarations
CubicThetaPrimeRowEquivalences.lean 5 declarations
CubicThetaPrimeRowRecurrence.lean 4 declarations
CubicThetaPrimeSectionEnergy.lean 7 declarations
CubicThetaPrimeSectionNorm.lean 7 declarations
CubicThetaPrimeSheetIntegral.lean 1 declarations
CubicThetaPrimeShiftRows.lean 9 declarations
CubicThetaPrimeSquareResidueZero.lean 1 declarations
CubicThetaPrimeSquareRows.lean 7 declarations
CubicThetaPrimeTraceEnergy.lean 9 declarations
CubicThetaPrimeTraceEnergyBound.lean 4 declarations
CubicThetaPrimeTraceFiniteEnergy.lean 6 declarations
CubicThetaPrimeTraceL2.lean 4 declarations
CubicThetaPrimeTraceLinear.lean 3 declarations
CubicThetaPrimeTraceNormBound.lean 7 declarations
CubicThetaPrimeTracePairing.lean 4 declarations
CubicThetaPrimeTraceRegularity.lean 2 declarations
CubicThetaPrimeTraceSection.lean 6 declarations
CubicThetaPrimeValuation.lean 6 declarations
CubicThetaPrimeWeakLift.lean 7 declarations
CubicThetaPrimitiveAction.lean 12 declarations
CubicThetaPrimitiveHeat.lean 9 declarations
CubicThetaPrimitiveHeatCusp.lean 7 declarations
CubicThetaPrimitiveHeatDecay.lean 5 declarations
CubicThetaPrimitiveKernel.lean 7 declarations
CubicThetaPrimitiveKernelBound.lean 3 declarations
CubicThetaPrimitivePower.lean 5 declarations
CubicThetaPrimitiveRowFactorization.lean 4 declarations
CubicThetaPrimitiveZeroRows.lean 7 declarations
CubicThetaPrincipalPart.lean 5 declarations
CubicThetaPrincipalTrace.lean 2 declarations
CubicThetaProjectedAngular.lean 1 declarations
CubicThetaProjectedAngularMellin.lean 9 declarations
CubicThetaProjectedCoefficient.lean 7 declarations
CubicThetaProjectedConstant.lean 5 declarations
CubicThetaProjectedContour.lean 1 declarations
CubicThetaProjectedDirichlet.lean 11 declarations
CubicThetaProjectedFiniteOrder.lean 3 declarations
CubicThetaProjectedFunctional.lean 5 declarations
CubicThetaProjectedLineBounds.lean 3 declarations
CubicThetaProjectedMultiplier.lean 3 declarations
CubicThetaProjectedPlane.lean 7 declarations
CubicThetaProjectedPolynomialStrip.lean 1 declarations
CubicThetaProjectedRadial.lean 12 declarations
CubicThetaProjectedRadialPoles.lean 9 declarations
CubicThetaProjectedSmoothMellin.lean 3 declarations
CubicThetaProjectedUpperBound.lean 3 declarations
CubicThetaProperAction.lean 8 declarations
CubicThetaQuadraticDerivatives.lean 8 declarations
CubicThetaQuotient.lean 9 declarations
CubicThetaQuotientCharts.lean 13 declarations
CubicThetaQuotientCore.lean 5 declarations
CubicThetaQuotientEnergy.lean 8 declarations
CubicThetaQuotientLocalFiniteness.lean 2 declarations
CubicThetaQuotientManifold.lean 2 declarations
CubicThetaQuotientMeasure.lean 6 declarations
CubicThetaRadialAverage.lean 3 declarations
CubicThetaRadialCompactInclusion.lean 3 declarations
CubicThetaRadialCompactness.lean 4 declarations
CubicThetaRadialConductor.lean 4 declarations
CubicThetaRadialContour.lean 2 declarations
CubicThetaRadialDirichlet.lean 10 declarations
CubicThetaRadialDual.lean 1 declarations
CubicThetaRadialDyadic.lean 1 declarations
CubicThetaRadialEnergy.lean 6 declarations
CubicThetaRadialEnergyNorm.lean 4 declarations
CubicThetaRadialEquicontinuity.lean 7 declarations
CubicThetaRadialEulerScaling.lean 3 declarations
CubicThetaRadialForm.lean 11 declarations
CubicThetaRadialGaussTail.lean 1 declarations
CubicThetaRadialGreen.lean 10 declarations
CubicThetaRadialGrowth.lean 7 declarations
CubicThetaRadialHeckeWeight.lean 5 declarations
CubicThetaRadialHeight.lean 5 declarations
CubicThetaRadialHeightNoStopBound.lean 1 declarations
CubicThetaRadialHolder.lean 2 declarations
CubicThetaRadialInverse.lean 1 declarations
CubicThetaRadialLocalCompact.lean 3 declarations
CubicThetaRadialLong.lean 2 declarations
CubicThetaRadialLongScale.lean 2 declarations
CubicThetaRadialLow.lean 1 declarations
CubicThetaRadialMainConstant.lean 6 declarations
CubicThetaRadialMean.lean 1 declarations
CubicThetaRadialMeanIntegral.lean 5 declarations
CubicThetaRadialMellin.lean 5 declarations
CubicThetaRadialMellinIdentity.lean 3 declarations
CubicThetaRadialMellinIntegrability.lean 2 declarations
CubicThetaRadialNegativeLong.lean 2 declarations
CubicThetaRadialNegativeTail.lean 1 declarations
CubicThetaRadialNoStopNegligible.lean 1 declarations
CubicThetaRadialNonzero.lean 3 declarations
CubicThetaRadialOrdinaryTail.lean 1 declarations
CubicThetaRadialPoleBound.lean 1 declarations
CubicThetaRadialPolynomialStrip.lean 2 declarations
CubicThetaRadialProductWindow.lean 1 declarations
CubicThetaRadialProfileAlgebra.lean 2 declarations
CubicThetaRadialProfileEquation.lean 6 declarations
CubicThetaRadialProfilePairing.lean 5 declarations
CubicThetaRadialProfileSeries.lean 10 declarations
CubicThetaRadialProfileSmooth.lean 3 declarations
CubicThetaRadialRawVoronoi.lean 7 declarations
CubicThetaRadialRealPositive.lean 2 declarations
CubicThetaRadialRegularization.lean 10 declarations
CubicThetaRadialResidue.lean 2 declarations
CubicThetaRadialRestrictedNoStopWindow.lean 1 declarations
CubicThetaRadialRiesz.lean 13 declarations
CubicThetaRadialScaleFirstNoStopTail.lean 1 declarations
CubicThetaRadialShortOuterWindow.lean 1 declarations
CubicThetaRadialSmoothMellin.lean 2 declarations
CubicThetaRadialTail.lean 4 declarations
CubicThetaRadialTent.lean 7 declarations
CubicThetaRadialTestMass.lean 4 declarations
CubicThetaRadialTypeIHeight.lean 1 declarations
CubicThetaRadialTypeIIntegral.lean 2 declarations
CubicThetaRadialTypeILow.lean 2 declarations
CubicThetaRadialUpperLowTailUniform.lean 1 declarations
CubicThetaRadialUpperNoStopNegligible.lean 1 declarations
CubicThetaRadialUpperNoStopRow.lean 1 declarations
CubicThetaRadialVoronoi.lean 2 declarations
CubicThetaRadialWeightScaling.lean 4 declarations
CubicThetaRamanujan.lean 5 declarations
CubicThetaRamanujanProduct.lean 4 declarations
CubicThetaRamifiedAllRows.lean 5 declarations
CubicThetaRamifiedCharacter.lean 5 declarations
CubicThetaRamifiedCharacterFourier.lean 2 declarations
CubicThetaRamifiedCoefficientScaling.lean 4 declarations
CubicThetaRamifiedCoefficientSupport.lean 7 declarations
CubicThetaRamifiedContraction.lean 7 declarations
CubicThetaRamifiedCoordinates.lean 3 declarations
CubicThetaRamifiedCubeRows.lean 1 declarations
CubicThetaRamifiedDenominator.lean 4 declarations
CubicThetaRamifiedDirichlet.lean 4 declarations
CubicThetaRamifiedDirichletCube.lean 3 declarations
CubicThetaRamifiedFinite.lean 3 declarations
CubicThetaRamifiedForcingPhase.lean 1 declarations
CubicThetaRamifiedIdeal.lean 6 declarations
CubicThetaRamifiedLowContinuation.lean 7 declarations
CubicThetaRamifiedLowFactor.lean 3 declarations
CubicThetaRamifiedLowRow.lean 2 declarations
CubicThetaRamifiedMass.lean 5 declarations
CubicThetaRamifiedMassSeries.lean 11 declarations
CubicThetaRamifiedMiddleSupport.lean 6 declarations
CubicThetaRamifiedMiddleValue.lean 4 declarations
CubicThetaRamifiedMissingClass.lean 5 declarations
CubicThetaRamifiedMissingCoefficient.lean 3 declarations
CubicThetaRamifiedMissingResidue.lean 3 declarations
CubicThetaRamifiedModel.lean 5 declarations
CubicThetaRamifiedNineGauss.lean 3 declarations
CubicThetaRamifiedPhaseEigen.lean 1 declarations
CubicThetaRamifiedPhaseRows.lean 8 declarations
CubicThetaRamifiedPhaseTransport.lean 2 declarations
CubicThetaRamifiedPrimaryContinuation.lean 5 declarations
CubicThetaRamifiedPrimaryFactor.lean 2 declarations
CubicThetaRamifiedPrimaryResidue.lean 4 declarations
CubicThetaRamifiedPrimarySeries.lean 5 declarations
CubicThetaRamifiedPrimarySupport.lean 3 declarations
CubicThetaRamifiedReduction.lean 5 declarations
CubicThetaRamifiedResidueFormula.lean 6 declarations
CubicThetaRamifiedResiduePeriodicity.lean 4 declarations
CubicThetaRamifiedResidueSystem.lean 9 declarations
CubicThetaRamifiedRowConductor.lean 5 declarations
CubicThetaRamifiedRowInflation.lean 5 declarations
CubicThetaRamifiedRowValue.lean 2 declarations
CubicThetaRamifiedSeries.lean 3 declarations
CubicThetaRamifiedThreeTwists.lean 3 declarations
CubicThetaRamifiedTopPhase.lean 4 declarations
CubicThetaRamifiedTopRow.lean 3 declarations
CubicThetaRamifiedTrace.lean 5 declarations
CubicThetaRamifiedUnitConductor.lean 5 declarations
CubicThetaRamifiedUnitCube.lean 4 declarations
CubicThetaRamifiedUnitGauss.lean 3 declarations
CubicThetaRamifiedUnitInflation.lean 4 declarations
CubicThetaRamifiedUnitOperator.lean 5 declarations
CubicThetaRamifiedUnitValue.lean 2 declarations
CubicThetaRankinConvergence.lean 3 declarations
CubicThetaRankinRadialMass.lean 4 declarations
CubicThetaRankinUnfold.lean 3 declarations
CubicThetaRationalCusp.lean 7 declarations
CubicThetaRawPairs.lean 4 declarations
CubicThetaRawVoronoi.lean 3 declarations
CubicThetaRegularHeatHigh.lean 4 declarations
CubicThetaRegularHeatLow.lean 5 declarations
CubicThetaRegularHeatPole.lean 5 declarations
CubicThetaRegularizedFourier.lean 6 declarations
CubicThetaRemainderWeights.lean 11 declarations
CubicThetaRemovableResidue.lean 3 declarations
CubicThetaResidueCRT.lean 6 declarations
CubicThetaResidueConstant.lean 2 declarations
CubicThetaResidueCount.lean 7 declarations
CubicThetaResidueCusps.lean 7 declarations
CubicThetaResidueInversion.lean 1 declarations
CubicThetaResidueKernelPairing.lean 3 declarations
CubicThetaResidueLocalCoefficient.lean 1 declarations
CubicThetaResidueMassPairing.lean 4 declarations
CubicThetaResidueNorm.lean 3 declarations
CubicThetaResidueNormalization.lean 6 declarations
CubicThetaResiduePrimarySupport.lean 3 declarations
CubicThetaResidueSourceOrbit.lean 6 declarations
CubicThetaResidueVanishing.lean 3 declarations
CubicThetaResidueWhittaker.lean 2 declarations
CubicThetaRestrictedNoStopWindow.lean 1 declarations
CubicThetaRowCompletionTranslation.lean 3 declarations
CubicThetaRowContinuation.lean 5 declarations
CubicThetaRowEntire.lean 3 declarations
CubicThetaRowFiniteFourier.lean 4 declarations
CubicThetaRowFourier.lean 4 declarations
CubicThetaRowFrequencyScaling.lean 4 declarations
CubicThetaRowGaussBounds.lean 7 declarations
CubicThetaRowGaussian.lean 3 declarations
CubicThetaRowHeightChain.lean 4 declarations
CubicThetaRowHeightEquation.lean 3 declarations
CubicThetaRowMellin.lean 3 declarations
CubicThetaRowPoisson.lean 3 declarations
CubicThetaRowRadius.lean 6 declarations
CubicThetaRowTranslationEquiv.lean 7 declarations
CubicThetaScalarCuspCutoff.lean 9 declarations
CubicThetaScalarCuspEnergy.lean 5 declarations
CubicThetaScalarCuspQuotient.lean 7 declarations
CubicThetaScalarCuspSupport.lean 5 declarations
CubicThetaScalarCuspVanishing.lean 3 declarations
CubicThetaScalarEisenstein.lean 4 declarations
CubicThetaScalarFactorization.lean 5 declarations
CubicThetaScalarGaussian.lean 3 declarations
CubicThetaScalarGaussianError.lean 3 declarations
CubicThetaScalarGaussianReal.lean 7 declarations
CubicThetaScalarHeightCutoff.lean 7 declarations
CubicThetaScalarHeightSeed.lean 8 declarations
CubicThetaScalarRankinKernel.lean 7 declarations
CubicThetaScalarRankinRadial.lean 3 declarations
CubicThetaScalarResidue.lean 1 declarations
CubicThetaScalarResidueReduction.lean 4 declarations
CubicThetaScalarSeedPairing.lean 12 declarations
CubicThetaScalarWindow.lean 9 declarations
CubicThetaScaleFirstNoStopTail.lean 1 declarations
CubicThetaScaledAngularMellin.lean 6 declarations
CubicThetaScaledCoefficientReduction.lean 3 declarations
CubicThetaScaledUpperMellin.lean 5 declarations
CubicThetaScatteringMeromorphic.lean 5 declarations
CubicThetaScatteringRegular.lean 3 declarations
CubicThetaScatteringRegularResidue.lean 1 declarations
CubicThetaScatteringResidue.lean 3 declarations
CubicThetaSecondChain.lean 1 declarations
CubicThetaSecondContinuity.lean 4 declarations
CubicThetaSectionCutoffEnergy.lean 2 declarations
CubicThetaSectionDifferential.lean 8 declarations
CubicThetaSectionFourierPairing.lean 5 declarations
CubicThetaSectionLocalization.lean 5 declarations
CubicThetaSectionMean.lean 4 declarations
CubicThetaSectionMeanPairing.lean 3 declarations
CubicThetaSectionPairing.lean 6 declarations
CubicThetaSelectedAngularMellin.lean 6 declarations
CubicThetaSelectedGaussSum.lean 5 declarations
CubicThetaSelectedOuter.lean 1 declarations
CubicThetaSelectedTransform.lean 1 declarations
CubicThetaSelectedVoronoi.lean 1 declarations
CubicThetaSeries.lean 8 declarations
CubicThetaShiftedCoefficientNormalization.lean 4 declarations
CubicThetaShiftedCoefficientPointwise.lean 3 declarations
CubicThetaShiftedCoefficients.lean 4 declarations
CubicThetaShiftedConstantCoefficient.lean 5 declarations
CubicThetaShiftedCuspGaussian.lean 2 declarations
CubicThetaShiftedCuspPeriodicity.lean 10 declarations
CubicThetaShiftedFourierSupport.lean 4 declarations
CubicThetaShiftedFrequencyBounds.lean 6 declarations
CubicThetaShiftedFrequencyContinuation.lean 4 declarations
CubicThetaShiftedFullFourier.lean 1 declarations
CubicThetaShiftedFullObservation.lean 7 declarations
CubicThetaShiftedFullResidue.lean 2 declarations
CubicThetaShiftedGaussExplicit.lean 6 declarations
CubicThetaShiftedGaussReduction.lean 6 declarations
CubicThetaShiftedHeatSummability.lean 6 declarations
CubicThetaShiftedHorizontalContinuity.lean 6 declarations
CubicThetaShiftedInvertedRows.lean 8 declarations
CubicThetaShiftedLattice.lean 9 declarations
CubicThetaShiftedModelPeriodicity.lean 2 declarations
CubicThetaShiftedModelSeries.lean 11 declarations
CubicThetaShiftedPeriodMeasure.lean 12 declarations
CubicThetaShiftedPositiveConstant.lean 4 declarations
CubicThetaShiftedPositivePairing.lean 2 declarations
CubicThetaShiftedPositivePointwise.lean 2 declarations
CubicThetaShiftedPositiveSeries.lean 4 declarations
CubicThetaShiftedRadialMellin.lean 7 declarations
CubicThetaShiftedResidueObservation.lean 3 declarations
CubicThetaShiftedResiduePairing.lean 4 declarations
CubicThetaShiftedRowFourier.lean 5 declarations
CubicThetaShiftedRowMellin.lean 6 declarations
CubicThetaShiftedRowWeight.lean 10 declarations
CubicThetaShiftedSeriesFunction.lean 7 declarations
CubicThetaShiftedSeriesIdentity.lean 4 declarations
CubicThetaShiftedTorus.lean 9 declarations
CubicThetaShiftedUnfold.lean 7 declarations
CubicThetaShiftedWeightFactor.lean 2 declarations
CubicThetaShiftedWhittaker.lean 2 declarations
CubicThetaShiftedWindow.lean 5 declarations
CubicThetaShiftedWindowFourier.lean 2 declarations
CubicThetaShiftedWindowTest.lean 10 declarations
CubicThetaShortInverse.lean 1 declarations
CubicThetaShortLogInverse.lean 1 declarations
CubicThetaShortModelLow.lean 1 declarations
CubicThetaShortOuterWindow.lean 1 declarations
CubicThetaSiegelReduction.lean 9 declarations
CubicThetaSievePhase.lean 8 declarations
CubicThetaSieveProjection.lean 8 declarations
CubicThetaSieveSupport.lean 10 declarations
CubicThetaSmoothChartWeak.lean 1 declarations
CubicThetaSmoothGlobalWeak.lean 3 declarations
CubicThetaSmoothLocalWeak.lean 3 declarations
CubicThetaSmoothMellin.lean 7 declarations
CubicThetaSmoothPairSupport.lean 2 declarations
CubicThetaSmoothTests.lean 5 declarations
CubicThetaSmoothWeakDefect.lean 4 declarations
CubicThetaSmoothingSupport.lean 1 declarations
CubicThetaSobolevEnergy.lean 6 declarations
CubicThetaSpatialContinuity.lean 4 declarations
CubicThetaSpatialDerivativeBound.lean 5 declarations
CubicThetaSpatialRegularity.lean 5 declarations
CubicThetaSpectralSimplePole.lean 8 declarations
CubicThetaSquareDecomposition.lean 5 declarations
CubicThetaSquarefreeMassEuler.lean 4 declarations
CubicThetaSquarefreeResidue.lean 1 declarations
CubicThetaStripFiniteVolume.lean 2 declarations
CubicThetaStripFourierSeparation.lean 2 declarations
CubicThetaStripHorizontalDensity.lean 4 declarations
CubicThetaStripRepresentative.lean 7 declarations
CubicThetaSupportedTangent.lean 6 declarations
CubicThetaSymbolKloostermanSymmetry.lean 3 declarations
CubicThetaTailCoordinates.lean 10 declarations
CubicThetaTailTerm.lean 5 declarations
CubicThetaTangentEnergy.lean 7 declarations
CubicThetaTangentIsometry.lean 7 declarations
CubicThetaTangentSobolev.lean 10 declarations
CubicThetaTangentVolume.lean 5 declarations
CubicThetaThetaObservation.lean 3 declarations
CubicThetaTorusCellIntegral.lean 2 declarations
CubicThetaTorusCellTransport.lean 6 declarations
CubicThetaTorusModes.lean 10 declarations
CubicThetaTorusSlices.lean 11 declarations
CubicThetaTotientConvolution.lean 6 declarations
CubicThetaTotientEuler.lean 7 declarations
CubicThetaTotientSeries.lean 6 declarations
CubicThetaTranslatedCuspStrip.lean 7 declarations
CubicThetaTwiceDifferentiation.lean 2 declarations
CubicThetaTwistFourier.lean 6 declarations
CubicThetaTypeILogCoefficients.lean 1 declarations
CubicThetaTypeILow.lean 2 declarations
CubicThetaTypeIMixedLow.lean 1 declarations
CubicThetaTypeIProductWindow.lean 4 declarations
CubicThetaUniformInverse.lean 1 declarations
CubicThetaUniformLong.lean 2 declarations
CubicThetaUniformMean.lean 1 declarations
CubicThetaUniformNegativeLong.lean 2 declarations
CubicThetaUniformNegativeMean.lean 1 declarations
CubicThetaUniformShort.lean 2 declarations
CubicThetaUniformSignedMean.lean 1 declarations
CubicThetaUnitCharacter.lean 4 declarations
CubicThetaUnitCharacterFourier.lean 4 declarations
CubicThetaUnitCount.lean 9 declarations
CubicThetaUnitLifting.lean 6 declarations
CubicThetaUnitPhaseSymbol.lean 8 declarations
CubicThetaUpperLowTailUniform.lean 1 declarations
CubicThetaUpperMellin.lean 6 declarations
CubicThetaUpperNoStopNegligible.lean 1 declarations
CubicThetaUpperNoStopRow.lean 1 declarations
CubicThetaVerticalDerivatives.lean 8 declarations
CubicThetaVerticalProduct.lean 2 declarations
CubicThetaVerticalSeriesDerivative.lean 2 declarations
CubicThetaVerticalTermDerivative.lean 4 declarations
CubicThetaVoronoiScale.lean 5 declarations
CubicThetaWeakUniqueness.lean 2 declarations
CubicThetaWeightFactor.lean 4 declarations
CubicThetaWeightedResidue.lean 5 declarations
CubicThetaWeightedTest.lean 8 declarations
CubicThetaWindowEquation.lean 4 declarations
CubicThetaWindowFlux.lean 8 declarations
CubicThetaWindowFluxIntegral.lean 5 declarations
CubicThetaWindowProfile.lean 14 declarations
CubicThetaWindowWeak.lean 8 declarations
CubicThetaWirtinger.lean 9 declarations
CubicThetaZeroFourier.lean 5 declarations
CubicThetaZeroObservable.lean 4 declarations
CubicThetaZeroRadialMellin.lean 5 declarations
CubicThetaZeroRadialPositive.lean 2 declarations
CubicThetaZeroWindow.lean 5 declarations