OAI/NumberTheory/DirichletL/Eisenstein/
3793 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- AffineCuspFourier.lean 26 declarations
- ArbitraryCuspPullback.lean 56 declarations
- BarrierPotential.lean 30 declarations
- BesselDerivatives.lean 34 declarations
- BesselMellinTransform.lean 39 declarations
- CompactEnergyFamilies.lean 45 declarations
- CompactProfiles.lean 41 declarations
- ConjugateCuspProfiles.lean 42 declarations
- ConjugateLevelAction.lean 57 declarations
- ConstantDirichletSeries.lean 36 declarations
- ConstantTermSupport.lean 28 declarations
- CoordinateLaplacian.lean 47 declarations
- CorrespondenceAdjoint.lean 42 declarations
- CorrespondenceEnergy.lean 34 declarations
- CorrespondencePullback.lean 34 declarations
- CorrespondenceTests.lean 34 declarations
- CoverTrace.lean 47 declarations
- CubeCuspAverage.lean 41 declarations
- CubeEigenrelation.lean 56 declarations
- CubeResidueStrata.lean 48 declarations
- CuspAverage.lean 37 declarations
- CuspDilation.lean 33 declarations
- CuspHeight.lean 71 declarations
- CuspIntegration.lean 62 declarations
- CuspResidues.lean 67 declarations
- CutoffApproximation.lean 38 declarations
- DirichletForm.lean 41 declarations
- EntireMellinProfile.lean 36 declarations
- FixedConductor.lean 46 declarations
- FixedCuspArrays.lean 55 declarations
- FixedFrequencyExpansion.lean 53 declarations
- FixedThetaTwists.lean 48 declarations
- FourierCoefficients.lean 51 declarations
- FredholmAlternative.lean 26 declarations
- FullFrequencyExpansion.lean 35 declarations
- FundamentalDomain.lean 64 declarations
- GaussFactorization.lean 37 declarations
- GreenIdentity.lean 48 declarations
- HyperbolicSpace.lean 58 declarations
- HyperbolicVolume.lean 61 declarations
- IntegralCover.lean 72 declarations
- InverseCorrespondence.lean 52 declarations
- InverseCuspCoordinates.lean 35 declarations
- LocalCutoffs.lean 41 declarations
- MeromorphicResolvent.lean 79 declarations
- OppositeCusp.lean 61 declarations
- PrimeGaussFactors.lean 34 declarations
- PrimePowerGaussSums.lean 47 declarations
- PrimeRecurrence.lean 33 declarations
- PrimitiveRows.lean 44 declarations
- QuotientTopology.lean 57 declarations
- RamifiedGaussSeries.lean 42 declarations
- RamifiedNormWeights.lean 40 declarations
- RamifiedSixBranches.lean 34 declarations
- RamifiedTransform.lean 39 declarations
- RamifiedValuation.lean 51 declarations
- RationalTranslations.lean 47 declarations
- ReflectedCuspMellin.lean 41 declarations
- ReflectionFibers.lean 43 declarations
- ResidualCuspDecay.lean 40 declarations
- ResidualFourierBounds.lean 42 declarations
- ResidualFourierExpansion.lean 46 declarations
- ResidualFourierSeries.lean 40 declarations
- ResidualOrthogonality.lean 39 declarations
- Rows.lean 84 declarations
- ScatteringCoefficients.lean 69 declarations
- ScatteringResidues.lean 44 declarations
- SeedDefects.lean 39 declarations
- SeedHeight.lean 50 declarations
- SmoothCuspCutoffs.lean 61 declarations
- SmoothSummands.lean 41 declarations
- SmoothTests.lean 43 declarations
- SourceBesselExpansion.lean 37 declarations
- SourceCuspKernels.lean 39 declarations
- SourceMellinInversion.lean 46 declarations
- SourceProjection.lean 62 declarations
- SourceQuotient.lean 63 declarations
- SquarefreeCoefficients.lean 44 declarations
- TranslatedFourierResidues.lean 38 declarations
- UnitNormalization.lean 43 declarations
- VariationalLaplacian.lean 61 declarations
- WhittakerContinuation.lean 46 declarations