OAI/NumberTheory/DirichletL/Foundation.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 286 imports below, so a file that imports it gets all of them.
Imports
- OAI.NumberTheory.DirichletL.Arithmetic.EisensteinCoordinates
- OAI.NumberTheory.DirichletL.Mellin.ExponentialSmoothing
- OAI.NumberTheory.DirichletL.Mellin.LogProfiles
- OAI.NumberTheory.DirichletL.ChineseRemainder.AdditiveCharacters
- OAI.NumberTheory.DirichletL.Arithmetic.EisensteinIdeals
- OAI.NumberTheory.DirichletL.Cusp.MatrixPhases
- OAI.NumberTheory.DirichletL.GaussSum.FiniteFourier
- OAI.NumberTheory.DirichletL.GaussSum.ChineseRemainder
- OAI.NumberTheory.DirichletL.Arithmetic.EisensteinEmbedding
- OAI.NumberTheory.DirichletL.GaussSum.CubicNormalization
- OAI.NumberTheory.DirichletL.GaussSum.SexticNormalization
- OAI.NumberTheory.DirichletL.GaussSum.LocalProductAssembly
- OAI.NumberTheory.DirichletL.GaussSum.RamifiedTracePhase
- OAI.NumberTheory.DirichletL.Arithmetic.LatticeCount
- OAI.NumberTheory.DirichletL.GaussSum.QuadraticTrace
- OAI.NumberTheory.DirichletL.GaussSum.QuadraticNormalization
- OAI.NumberTheory.DirichletL.Poisson.BinaryGaussian
- OAI.NumberTheory.DirichletL.GaussSum.GaussianDualLimit
- OAI.NumberTheory.DirichletL.GaussSum.GaussianFiberMass
- OAI.NumberTheory.DirichletL.Poisson.GaussianMoments
- OAI.NumberTheory.DirichletL.Poisson.OscillatoryGaussian
- OAI.NumberTheory.DirichletL.PrimeRows.RationalApproximation
- OAI.NumberTheory.DirichletL.GaussSum.AbelPhaseLimit
- OAI.NumberTheory.DirichletL.GaussSum.ThetaLocalRows
- OAI.NumberTheory.DirichletL.Mellin.LocalNonvanishing
- OAI.NumberTheory.DirichletL.Arithmetic.NormFiberMellin
- OAI.NumberTheory.DirichletL.Hecke.NormFiberCharacters
- OAI.NumberTheory.DirichletL.Hecke.LocalEulerIdentities
- OAI.NumberTheory.DirichletL.Hecke.PrimeExtraction
- OAI.NumberTheory.DirichletL.Mellin.FiniteEulerRestoration
- OAI.NumberTheory.DirichletL.PrimeRows.NormFiberExtraction
- OAI.NumberTheory.DirichletL.Hecke.FiniteEulerFactors
- OAI.NumberTheory.DirichletL.Mellin.CompactScale
- OAI.NumberTheory.DirichletL.Mellin.CompactWeights
- OAI.NumberTheory.DirichletL.Fourier.PositiveLogProfiles
- OAI.NumberTheory.DirichletL.GaussSum.SecondPoissonScale
- OAI.NumberTheory.DirichletL.Poisson.EisensteinLattice
- OAI.NumberTheory.DirichletL.GaussSum.SexticRadialPoisson
- OAI.NumberTheory.DirichletL.PrimeRows.IdealGenerators
- OAI.NumberTheory.DirichletL.PrimeRows.ActiveGaussFactorization
- OAI.NumberTheory.DirichletL.Poisson.RadialFourier
- OAI.NumberTheory.DirichletL.GaussSum.ActiveConductor
- OAI.NumberTheory.DirichletL.GaussSum.CubicTrace
- OAI.NumberTheory.DirichletL.GaussSum.MixedConversion
- OAI.NumberTheory.DirichletL.GaussSum.SquarePhaseFactorization
- OAI.NumberTheory.DirichletL.QuadraticSieve.CrossSeparation
- OAI.NumberTheory.DirichletL.Arithmetic.IdealMobius
- OAI.NumberTheory.DirichletL.GaussSum.CompletedExpansion
- OAI.NumberTheory.DirichletL.GaussSum.RayCharacters
- OAI.NumberTheory.DirichletL.QuadraticSieve.CoefficientCancellation
- OAI.NumberTheory.DirichletL.QuadraticSieve.InitialBound
- OAI.NumberTheory.DirichletL.Mellin.ReflectedKernel
- OAI.NumberTheory.DirichletL.Arithmetic.SquarefreeDivisors
- OAI.NumberTheory.DirichletL.QuadraticSieve.FiniteOperator
- OAI.NumberTheory.DirichletL.CubicSieve.CubeLabels
- OAI.NumberTheory.DirichletL.QuadraticSieve.MainTermDifference
- OAI.NumberTheory.DirichletL.Mellin.InverseContour
- OAI.NumberTheory.DirichletL.Mellin.UniformKernelBounds
- OAI.NumberTheory.DirichletL.CubicSieve.CrossFactorization
- OAI.NumberTheory.DirichletL.CubicSieve.LocalBrackets
- OAI.NumberTheory.DirichletL.GaussSum.ReflectionBrackets
- OAI.NumberTheory.DirichletL.CubicSieve.RayExpansion
- OAI.NumberTheory.DirichletL.QuadraticSieve.CoprimeBilinearBound
- OAI.NumberTheory.DirichletL.QuadraticSieve.IdealQuotients
- OAI.NumberTheory.DirichletL.CubicSieve.KernelEnergy
- OAI.NumberTheory.DirichletL.Reciprocity.CubicJacobi
- OAI.NumberTheory.DirichletL.Reciprocity.RamifiedSymbol
- OAI.NumberTheory.DirichletL.Poisson.QuadraticProfiles
- OAI.NumberTheory.DirichletL.CubicSieve.FirstPassage
- OAI.NumberTheory.DirichletL.CubicSieve.RayCoefficients
- OAI.NumberTheory.DirichletL.QuadraticSieve.DivisorBlocks
- OAI.NumberTheory.DirichletL.CubicSieve.SecondPoisson
- OAI.NumberTheory.DirichletL.Eisenstein.Rows
- OAI.NumberTheory.DirichletL.Eisenstein.HyperbolicSpace
- OAI.NumberTheory.DirichletL.Eisenstein.PrimitiveRows
- OAI.NumberTheory.DirichletL.Poisson.PrincipalTruncation
- OAI.NumberTheory.DirichletL.Fourier.FrequencyTwists
- OAI.NumberTheory.DirichletL.CubicSieve.ChildTransfer
- OAI.NumberTheory.DirichletL.CubicSieve.IntegratedTransfer
- OAI.NumberTheory.DirichletL.Fourier.TupleWeights
- OAI.NumberTheory.DirichletL.QuadraticSieve.GcdReduction
- OAI.NumberTheory.DirichletL.QuadraticSieve.AnnularRecursion
- OAI.NumberTheory.DirichletL.CubicSieve.RowMajorants
- OAI.NumberTheory.DirichletL.Eisenstein.FourierCoefficients
- OAI.NumberTheory.DirichletL.QuadraticSieve.PrimePools
- OAI.NumberTheory.DirichletL.CubicSieve.FrequencyBlocks
- OAI.NumberTheory.DirichletL.CubicSieve.FixedProfiles
- OAI.NumberTheory.DirichletL.Eisenstein.ConstantTermSupport
- OAI.NumberTheory.DirichletL.QuadraticSieve.SquareParts
- OAI.NumberTheory.DirichletL.CubicSieve.ResidualSectors
- OAI.NumberTheory.DirichletL.QuadraticSieve.UnrestrictedCharacters
- OAI.NumberTheory.DirichletL.CubicSieve.ConjugateProfiles
- OAI.NumberTheory.DirichletL.Eisenstein.RamifiedNormWeights
- OAI.NumberTheory.DirichletL.QuadraticSieve.PrincipalTruncation
- OAI.NumberTheory.DirichletL.CubicSieve.FrequencyCutoffs
- OAI.NumberTheory.DirichletL.Eisenstein.ConstantDirichletSeries
- OAI.NumberTheory.DirichletL.QuadraticSieve.DyadicColumns
- OAI.NumberTheory.DirichletL.QuadraticSieve.TruncatedSecondTransfer
- OAI.NumberTheory.DirichletL.CubicSieve.TwistedProfiles
- OAI.NumberTheory.DirichletL.Fourier.LogDensity
- OAI.NumberTheory.DirichletL.QuadraticSieve.PrincipalDifference
- OAI.NumberTheory.DirichletL.CubicSieve.FirstCoreCutoff
- OAI.NumberTheory.DirichletL.QuadraticSieve.SpatialDerivatives
- OAI.NumberTheory.DirichletL.Eisenstein.SmoothSummands
- OAI.NumberTheory.DirichletL.Poisson.LatticeEnvelopes
- OAI.NumberTheory.DirichletL.CubicSieve.SupportNorms
- OAI.NumberTheory.DirichletL.QuadraticSieve.MiddleWindows
- OAI.NumberTheory.DirichletL.QuadraticSieve.GreenIntegrals
- OAI.NumberTheory.DirichletL.Eisenstein.GreenIdentity
- OAI.NumberTheory.DirichletL.CubicSieve.LogarithmicTargets
- OAI.NumberTheory.DirichletL.Eisenstein.CuspIntegration
- OAI.NumberTheory.DirichletL.QuadraticSieve.DualMiddleExpansion
- OAI.NumberTheory.DirichletL.QuadraticSieve.MaskedPrincipalBounds
- OAI.NumberTheory.DirichletL.QuadraticSieve.LogarithmicSectors
- OAI.NumberTheory.DirichletL.CubicSieve.SquarefreeTransfer
- OAI.NumberTheory.DirichletL.Eisenstein.SmoothCuspCutoffs
- OAI.NumberTheory.DirichletL.Eisenstein.SeedDefects
- OAI.NumberTheory.DirichletL.CubicSieve.GlobalEncoding
- OAI.NumberTheory.DirichletL.CubicSieve.PrincipalNormalization
- OAI.NumberTheory.DirichletL.QuadraticSieve.PrincipalMajorants
- OAI.NumberTheory.DirichletL.QuadraticSieve.RetainedDualBounds
- OAI.NumberTheory.DirichletL.QuadraticSieve.HighKernelGeometry
- OAI.NumberTheory.DirichletL.Eisenstein.QuotientTopology
- OAI.NumberTheory.DirichletL.CubicSieve.PrincipalDensity
- OAI.NumberTheory.DirichletL.QuadraticSieve.CuspCoercivity
- OAI.NumberTheory.DirichletL.QuadraticSieve.CommonMasks
- OAI.NumberTheory.DirichletL.CubicSieve.ScaleCaps
- OAI.NumberTheory.DirichletL.QuadraticSieve.PoissonComparison
- OAI.NumberTheory.DirichletL.CubicSieve.ArithmeticBins
- OAI.NumberTheory.DirichletL.Eisenstein.HyperbolicVolume
- OAI.NumberTheory.DirichletL.CubicSieve.UniformTransfer
- OAI.NumberTheory.DirichletL.QuadraticSieve.GlobalBinLoss
- OAI.NumberTheory.DirichletL.Eisenstein.FundamentalDomain
- OAI.NumberTheory.DirichletL.GaussSum.GlobalScales
- OAI.NumberTheory.DirichletL.QuadraticSieve.AnnularLifting
- OAI.NumberTheory.DirichletL.QuadraticSieve.PoissonConstants
- OAI.NumberTheory.DirichletL.QuadraticSieve.SelectedExponents
- OAI.NumberTheory.DirichletL.QuadraticSieve.LogarithmicLoss
- OAI.NumberTheory.DirichletL.Eisenstein.CompactProfiles
- OAI.NumberTheory.DirichletL.CubicSieve.LiteralSources
- OAI.NumberTheory.DirichletL.CubicSieve.PooledRows
- OAI.NumberTheory.DirichletL.MeanSquare.TransformedColumns
- OAI.NumberTheory.DirichletL.QuadraticSieve.ProductColumns
- OAI.NumberTheory.DirichletL.QuadraticSieve.UniformTailBounds
- OAI.NumberTheory.DirichletL.CubicSieve.CubeBlocks
- OAI.NumberTheory.DirichletL.GaussSum.PowerfulParts
- OAI.NumberTheory.DirichletL.MeanSquare.SourceTransfer
- OAI.NumberTheory.DirichletL.MeanSquare.LogarithmicBins
- OAI.NumberTheory.DirichletL.CubicSieve.RowCaps
- OAI.NumberTheory.DirichletL.Eisenstein.SmoothTests
- OAI.NumberTheory.DirichletL.CubicSieve.DivisorTargets
- OAI.NumberTheory.DirichletL.CubicSieve.NormalizedMass
- OAI.NumberTheory.DirichletL.GaussSum.ReflectedBranches
- OAI.NumberTheory.DirichletL.Eisenstein.DirichletForm
- OAI.NumberTheory.DirichletL.MeanSquare.InputEnergy
- OAI.NumberTheory.DirichletL.CubicSieve.QuantitativePassage
- OAI.NumberTheory.DirichletL.MeanSquare.OutsideIdeals
- OAI.NumberTheory.DirichletL.MeanSquare.PoissonSource
- OAI.NumberTheory.DirichletL.CubicSieve.DyadicKernel
- OAI.NumberTheory.DirichletL.MeanSquare.ReflectedDyadicSeries
- OAI.NumberTheory.DirichletL.GaussSum.BranchScaling
- OAI.NumberTheory.DirichletL.CubicSieve.RadialWindows
- OAI.NumberTheory.DirichletL.Eisenstein.LocalCutoffs
- OAI.NumberTheory.DirichletL.GaussSum.CompletedDyadicRows
- OAI.NumberTheory.DirichletL.MeanSquare.HarmonicAggregation
- OAI.NumberTheory.DirichletL.CubicSieve.PaddedPassage
- OAI.NumberTheory.DirichletL.MeanSquare.DiagonalDensity
- OAI.NumberTheory.DirichletL.MeanSquare.HighRadialBounds
- OAI.NumberTheory.DirichletL.MeanSquare.SourceRemainders
- OAI.NumberTheory.DirichletL.CubicSieve.DualZeroMode
- OAI.NumberTheory.DirichletL.Eisenstein.VariationalLaplacian
- OAI.NumberTheory.DirichletL.MeanSquare.CanonicalDensity
- OAI.NumberTheory.DirichletL.MeanSquare.RetainedDensity
- OAI.NumberTheory.DirichletL.MeanSquare.CanonicalTailBounds
- OAI.NumberTheory.DirichletL.CubicSieve.ReopenedFibers
- OAI.NumberTheory.DirichletL.Eisenstein.CompactEnergyFamilies
- OAI.NumberTheory.DirichletL.RowCompletion.SupportBounds
- OAI.NumberTheory.DirichletL.CubicSieve.ReopeningSeparation
- OAI.NumberTheory.DirichletL.CubicSieve.LogSeparation
- OAI.NumberTheory.DirichletL.CubicSieve.CanonicalLogEnergy
- OAI.NumberTheory.DirichletL.CubicSieve.RadialProfiles
- OAI.NumberTheory.DirichletL.RowCompletion.PolynomialHeight
- OAI.NumberTheory.DirichletL.MeanSquare.PolynomialHeight
- OAI.NumberTheory.DirichletL.Eisenstein.CoordinateLaplacian
- OAI.NumberTheory.DirichletL.CubicSieve.DensityBudgets
- OAI.NumberTheory.DirichletL.CubicSieve.RankMargins
- OAI.NumberTheory.DirichletL.MeanSquare.UniformPolynomialHeight
- OAI.NumberTheory.DirichletL.MeanSquare.UnitRows
- OAI.NumberTheory.DirichletL.Eisenstein.CuspHeight
- OAI.NumberTheory.DirichletL.Eisenstein.BarrierPotential
- OAI.NumberTheory.DirichletL.CubicSieve.ReopeningBounds
- OAI.NumberTheory.DirichletL.CubicSieve.CutoffOrders
- OAI.NumberTheory.DirichletL.CubicSieve.ClosedRecursion
- OAI.NumberTheory.DirichletL.Eisenstein.FredholmAlternative
- OAI.NumberTheory.DirichletL.Eisenstein.UnitNormalization
- OAI.NumberTheory.DirichletL.RowCompletion.CubicReopening
- OAI.NumberTheory.DirichletL.RowCompletion.CompletedEnergy
- OAI.NumberTheory.DirichletL.Eisenstein.MeromorphicResolvent
- OAI.NumberTheory.DirichletL.RowCompletion.DensityTransfer
- OAI.NumberTheory.DirichletL.Eisenstein.SeedHeight
- OAI.NumberTheory.DirichletL.RowCompletion.InitialDensity
- OAI.NumberTheory.DirichletL.MeanSquare.ThetaDensity
- OAI.NumberTheory.DirichletL.Mellin.SixthPowerAverage
- OAI.NumberTheory.DirichletL.Hecke.MobiusEulerCorrection
- OAI.NumberTheory.DirichletL.RowCompletion.ThetaNonvanishing
- OAI.NumberTheory.DirichletL.Eisenstein.CutoffApproximation
- OAI.NumberTheory.DirichletL.Eisenstein.CuspResidues
- OAI.NumberTheory.DirichletL.Eisenstein.ConjugateLevelAction
- OAI.NumberTheory.DirichletL.Eisenstein.ScatteringCoefficients
- OAI.NumberTheory.DirichletL.Eisenstein.WhittakerContinuation
- OAI.NumberTheory.DirichletL.Eisenstein.GaussFactorization
- OAI.NumberTheory.DirichletL.Reciprocity.KubotaCharacter
- OAI.NumberTheory.DirichletL.Eisenstein.ResidualFourierBounds
- OAI.NumberTheory.DirichletL.Eisenstein.RamifiedGaussSeries
- OAI.NumberTheory.DirichletL.Eisenstein.SourceProjection
- OAI.NumberTheory.DirichletL.Eisenstein.SourceQuotient
- OAI.NumberTheory.DirichletL.Eisenstein.ResidualFourierSeries
- OAI.NumberTheory.DirichletL.Eisenstein.ScatteringResidues
- OAI.NumberTheory.DirichletL.Eisenstein.OppositeCusp
- OAI.NumberTheory.DirichletL.Eisenstein.ResidualFourierExpansion
- OAI.NumberTheory.DirichletL.Eisenstein.RationalTranslations
- OAI.NumberTheory.DirichletL.Eisenstein.CuspAverage
- OAI.NumberTheory.DirichletL.Eisenstein.BesselMellinTransform
- OAI.NumberTheory.DirichletL.Eisenstein.TranslatedFourierResidues
- OAI.NumberTheory.DirichletL.Eisenstein.ResidualCuspDecay
- OAI.NumberTheory.DirichletL.Eisenstein.PrimePowerGaussSums
- OAI.NumberTheory.DirichletL.Eisenstein.SourceBesselExpansion
- OAI.NumberTheory.DirichletL.Eisenstein.BesselDerivatives
- OAI.NumberTheory.DirichletL.Eisenstein.InverseCuspCoordinates
- OAI.NumberTheory.DirichletL.Eisenstein.ReflectedCuspMellin
- OAI.NumberTheory.DirichletL.Eisenstein.ArbitraryCuspPullback
- OAI.NumberTheory.DirichletL.Reciprocity.CubeCorrespondence
- OAI.NumberTheory.DirichletL.Eisenstein.ConjugateCuspProfiles
- OAI.NumberTheory.DirichletL.Eisenstein.CuspDilation
- OAI.NumberTheory.DirichletL.Cusp.ResiduesModThree
- OAI.NumberTheory.DirichletL.Reciprocity.PrimaryCongruences
- OAI.NumberTheory.DirichletL.Eisenstein.CubeResidueStrata
- OAI.NumberTheory.DirichletL.Reciprocity.RamifiedCuspPhases
- OAI.NumberTheory.DirichletL.Eisenstein.AffineCuspFourier
- OAI.NumberTheory.DirichletL.Eisenstein.IntegralCover
- OAI.NumberTheory.DirichletL.Eisenstein.CoverTrace
- OAI.NumberTheory.DirichletL.Eisenstein.CubeCuspAverage
- OAI.NumberTheory.DirichletL.Eisenstein.InverseCorrespondence
- OAI.NumberTheory.DirichletL.Eisenstein.CorrespondenceTests
- OAI.NumberTheory.DirichletL.Eisenstein.CorrespondencePullback
- OAI.NumberTheory.DirichletL.Eisenstein.RamifiedSixBranches
- OAI.NumberTheory.DirichletL.Eisenstein.CorrespondenceAdjoint
- OAI.NumberTheory.DirichletL.Eisenstein.CorrespondenceEnergy
- OAI.NumberTheory.DirichletL.Eisenstein.CubeEigenrelation
- OAI.NumberTheory.DirichletL.Eisenstein.ResidualOrthogonality
- OAI.NumberTheory.DirichletL.Eisenstein.PrimeRecurrence
- OAI.NumberTheory.DirichletL.Eisenstein.PrimeGaussFactors
- OAI.NumberTheory.DirichletL.Eisenstein.SquarefreeCoefficients
- OAI.NumberTheory.DirichletL.Eisenstein.SourceMellinInversion
- OAI.NumberTheory.DirichletL.GaussSum.DualKernelSummability
- OAI.NumberTheory.DirichletL.Mellin.VerticalContourShift
- OAI.NumberTheory.DirichletL.GaussSum.BesselReflection
- OAI.NumberTheory.DirichletL.GaussSum.FiniteTranslations
- OAI.NumberTheory.DirichletL.GaussSum.MellinSupport
- OAI.NumberTheory.DirichletL.Eisenstein.RamifiedTransform
- OAI.NumberTheory.DirichletL.Eisenstein.EntireMellinProfile
- OAI.NumberTheory.DirichletL.Eisenstein.RamifiedValuation
- OAI.NumberTheory.DirichletL.Eisenstein.SourceCuspKernels
- OAI.NumberTheory.DirichletL.Eisenstein.FullFrequencyExpansion
- OAI.NumberTheory.DirichletL.Eisenstein.FixedCuspArrays
- OAI.NumberTheory.DirichletL.Cusp.WeylRepresentatives
- OAI.NumberTheory.DirichletL.ChineseRemainder.PrimaryCompletions
- OAI.NumberTheory.DirichletL.Cusp.ResiduePhases
- OAI.NumberTheory.DirichletL.ChineseRemainder.FrequencyLifts
- OAI.NumberTheory.DirichletL.RowCompletion.PeriodicRows
- OAI.NumberTheory.DirichletL.GaussSum.ReflectionPool
- OAI.NumberTheory.DirichletL.Eisenstein.FixedConductor
- OAI.NumberTheory.DirichletL.RowCompletion.FixedCuspBranches
- OAI.NumberTheory.DirichletL.Cusp.StaticReflectionPhases
- OAI.NumberTheory.DirichletL.Eisenstein.FixedFrequencyExpansion
- OAI.NumberTheory.DirichletL.Eisenstein.FixedThetaTwists
- OAI.NumberTheory.DirichletL.GaussSum.FixedRayFibers
- OAI.NumberTheory.DirichletL.Eisenstein.ReflectionFibers
- OAI.NumberTheory.DirichletL.RowCompletion.ControlledPrimeStrata
- OAI.NumberTheory.DirichletL.RowCompletion.FreePrimePools
- OAI.NumberTheory.DirichletL.GaussSum.ResidualEquivalence
- OAI.NumberTheory.DirichletL.RowCompletion.RowAmplitudes
- OAI.NumberTheory.DirichletL.GaussSum.ActiveReindexing
- OAI.NumberTheory.DirichletL.RowCompletion.ReflectedFibers
- OAI.NumberTheory.DirichletL.RowCompletion.BranchDecoding
- OAI.NumberTheory.DirichletL.RowCompletion.ZeroFreeRegion
Imported by 41 files
- OAI/NumberTheory/DirichletL/CenteredExceptionalCount.lean
- OAI/NumberTheory/DirichletL/CompactProfileFamily.lean
- OAI/NumberTheory/DirichletL/CubicSieve/Ideal.lean
- OAI/NumberTheory/DirichletL/CubicSieve/Poisson.lean
- OAI/NumberTheory/DirichletL/Descent/Completion.lean
- OAI/NumberTheory/DirichletL/Descent/DescentProfiles.lean
- OAI/NumberTheory/DirichletL/Descent/IdealMasks.lean
- OAI/NumberTheory/DirichletL/Descent/Poisson.lean
- OAI/NumberTheory/DirichletL/Descent/PoissonTails.lean
- OAI/NumberTheory/DirichletL/Descent/Quadratic.lean
- OAI/NumberTheory/DirichletL/Descent/Widths.lean
- OAI/NumberTheory/DirichletL/Detector/Completed.lean
- OAI/NumberTheory/DirichletL/Detector/GramAnnularLattice.lean
- OAI/NumberTheory/DirichletL/Detector/GramFrequencySummation.lean
- OAI/NumberTheory/DirichletL/Detector/GramIdealSummation.lean
- OAI/NumberTheory/DirichletL/Detector/GramJointConstruction.lean
- OAI/NumberTheory/DirichletL/Detector/GramJointProfile.lean
- OAI/NumberTheory/DirichletL/Detector/GramLatticeDecay.lean
- OAI/NumberTheory/DirichletL/Detector/GramPeriodicPoisson.lean
- OAI/NumberTheory/DirichletL/Detector/Phase.lean
- OAI/NumberTheory/DirichletL/Detector/Physical.lean
- OAI/NumberTheory/DirichletL/Detector/PrimePower.lean
- OAI/NumberTheory/DirichletL/Detector/RadialMellin.lean
- OAI/NumberTheory/DirichletL/Detector/Row.lean
- OAI/NumberTheory/DirichletL/GammaZeroDetector.lean
- OAI/NumberTheory/DirichletL/Hecke/DetectorProfiles.lean
- OAI/NumberTheory/DirichletL/Hecke/IdealBridge.lean
- OAI/NumberTheory/DirichletL/IdealEuler.lean
- OAI/NumberTheory/DirichletL/Inversion/CanonicalReferenceThreshold.lean
- OAI/NumberTheory/DirichletL/Inversion/InitialFibers.lean
- OAI/NumberTheory/DirichletL/Inversion/InitialOverlap.lean
- OAI/NumberTheory/DirichletL/Inversion/KernelSourceUniform.lean
- OAI/NumberTheory/DirichletL/Moments/Canonical.lean
- OAI/NumberTheory/DirichletL/Moments/Lattice.lean
- OAI/NumberTheory/DirichletL/Moments/Mask.lean
- OAI/NumberTheory/DirichletL/Moments/Primary.lean
- OAI/NumberTheory/DirichletL/Nonvanishing.lean
- OAI/NumberTheory/DirichletL/ParametersProbeWindows.lean
- OAI/NumberTheory/DirichletL/Reflection/PowerfulBudget.lean
- OAI/NumberTheory/DirichletL/TraceCharacter.lean
- OAI/NumberTheory/DirichletL/UnitSexticWitness.lean