Documentation
LeanPool
.
LeanModularForms
.
Imports
Search
return to top
source
Imports
Init
LeanPool.LeanModularForms
LeanPool.LeanModularForms.ContourIntegral.CrossingLimit
LeanPool.LeanModularForms.ContourIntegral.PVSplit
LeanPool.LeanModularForms.ContourIntegral.SegmentFTC
LeanPool.LeanModularForms.ContourIntegral.WindingNumber
LeanPool.LeanModularForms.ForMathlib.AtImInfty
LeanPool.LeanModularForms.ForMathlib.Bounds
LeanPool.LeanModularForms.ForMathlib.CongruenceSubgroupsCopy
LeanPool.LeanModularForms.ForMathlib.CongruenceSubgrps
LeanPool.LeanModularForms.ForMathlib.FunctionsBoundedAtInfty
LeanPool.LeanModularForms.ForMathlib.Hassumunifon
LeanPool.LeanModularForms.ForMathlib.Identities
LeanPool.LeanModularForms.ForMathlib.Instances
LeanPool.LeanModularForms.ForMathlib.IsBoundedAtImInfty
LeanPool.LeanModularForms.ForMathlib.LevelOne
LeanPool.LeanModularForms.ForMathlib.Petersson
LeanPool.LeanModularForms.ForMathlib.QExpansion
LeanPool.LeanModularForms.ForMathlib.SlashActions
LeanPool.LeanModularForms.ForMathlib.UpperHalfPlane
LeanPool.LeanModularForms.GeneralizedResidueTheory.ArcCalculus
LeanPool.LeanModularForms.GeneralizedResidueTheory.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.Bridges
LeanPool.LeanModularForms.GeneralizedResidueTheory.CauchyPrimitive
LeanPool.LeanModularForms.GeneralizedResidueTheory.CurveAvoidance
LeanPool.LeanModularForms.GeneralizedResidueTheory.Cycle
LeanPool.LeanModularForms.GeneralizedResidueTheory.GeneralizedResidueTheorem
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy
LeanPool.LeanModularForms.GeneralizedResidueTheory.LogDerivFTC
LeanPool.LeanModularForms.GeneralizedResidueTheory.PiecewiseCurveAPI
LeanPool.LeanModularForms.GeneralizedResidueTheory.PrincipalValue
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing
LeanPool.LeanModularForms.Modularforms.AtImInfty
LeanPool.LeanModularForms.Modularforms.BigO
LeanPool.LeanModularForms.Modularforms.Cauchylems
LeanPool.LeanModularForms.Modularforms.ClogArgLems
LeanPool.LeanModularForms.Modularforms.Cotangent
LeanPool.LeanModularForms.Modularforms.Csqrt
LeanPool.LeanModularForms.Modularforms.Delta
LeanPool.LeanModularForms.Modularforms.Derivative
LeanPool.LeanModularForms.Modularforms.DimensionFormulas
LeanPool.LeanModularForms.Modularforms.E2
LeanPool.LeanModularForms.Modularforms.Eisenstein
LeanPool.LeanModularForms.Modularforms.EisensteinAsymptotics
LeanPool.LeanModularForms.Modularforms.Eisensteinqexpansions
LeanPool.LeanModularForms.Modularforms.Equivs
LeanPool.LeanModularForms.Modularforms.Eta
LeanPool.LeanModularForms.Modularforms.EtaCleanup
LeanPool.LeanModularForms.Modularforms.ExpLems
LeanPool.LeanModularForms.Modularforms.ForMathlibCusps
LeanPool.LeanModularForms.Modularforms.ForMathlibFunctionsBoundedAtInfty
LeanPool.LeanModularForms.Modularforms.ForMathlibSlashActions
LeanPool.LeanModularForms.Modularforms.ForMathlibUpperHalfPlane
LeanPool.LeanModularForms.Modularforms.Generators
LeanPool.LeanModularForms.Modularforms.IccIcoLems
LeanPool.LeanModularForms.Modularforms.IsCuspForm
LeanPool.LeanModularForms.Modularforms.Iteratedderivs
LeanPool.LeanModularForms.Modularforms.JacobiTheta
LeanPool.LeanModularForms.Modularforms.LimunderLems
LeanPool.LeanModularForms.Modularforms.LogDerivLems
LeanPool.LeanModularForms.Modularforms.MDifferentiableFunProp
LeanPool.LeanModularForms.Modularforms.MultipliableLems
LeanPool.LeanModularForms.Modularforms.PhiTransform
LeanPool.LeanModularForms.Modularforms.QExpansion
LeanPool.LeanModularForms.Modularforms.QExpansionLems
LeanPool.LeanModularForms.Modularforms.RamanujanIdentities
LeanPool.LeanModularForms.Modularforms.ResToImagAxis
LeanPool.LeanModularForms.Modularforms.RiemannZetalems
LeanPool.LeanModularForms.Modularforms.SerreDerivativeSlash
LeanPool.LeanModularForms.Modularforms.SlashActionAuxil
LeanPool.LeanModularForms.Modularforms.SummableLems
LeanPool.LeanModularForms.Modularforms.Tendstolems
LeanPool.LeanModularForms.Modularforms.ThetaDerivIdentities
LeanPool.LeanModularForms.Modularforms.TsumderivWithin
LeanPool.LeanModularForms.Modularforms.Uniformcts
LeanPool.LeanModularForms.Modularforms.Upperhalfplane
LeanPool.LeanModularForms.SpherePacking.CuspDecay
LeanPool.LeanModularForms.SpherePacking.PhiHolomorphic
LeanPool.LeanModularForms.SpherePacking.ViazovskaMagicFunction
LeanPool.LeanModularForms.ValenceFormula.CoreIdentity
LeanPool.LeanModularForms.ValenceFormula.Definitions
LeanPool.LeanModularForms.ValenceFormula.InteriorWinding
LeanPool.LeanModularForms.ValenceFormula.ModularInvariance
LeanPool.LeanModularForms.ValenceFormula.OrbitPairing
LeanPool.LeanModularForms.ValenceFormula.OrbitSum
LeanPool.LeanModularForms.ValenceFormula.PVChain
LeanPool.LeanModularForms.ValenceFormula.TextbookExistence
LeanPool.LeanModularForms.ValenceFormula.TextbookForm
LeanPool.LeanModularForms.ValenceFormula.TrigLemmas
LeanPool.LeanModularForms.ValenceFormula.WindingWeights
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.DixonProof
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.Meromorphic
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.CircleParam
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.Integrality
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.Invariance
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.MathlibBridge
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.ParametricDiff
LeanPool.LeanModularForms.GeneralizedResidueTheory.OnCurvePV.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.AnnulusBounds
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.GammaAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.RemainderAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.SingularAnnulus
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.StepBounds
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.UniformStepBound
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.Flatness
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.GeneralizedTheorem
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.GeneralizedTheoremBase
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MathlibBridge
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeasureHelpers
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeromorphicLaurent
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeromorphicPrincipalPart
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MultipointPV
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.SectorCurve
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.SectorCurveLemma
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.CrossingAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Decomposition
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Defs
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Proposition22
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Associativity
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Basic
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Commutativity
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Degree
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Module
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Multiplication
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Ring
LeanPool.LeanModularForms.HeckeRIngs.GL2.Basic
LeanPool.LeanModularForms.HeckeRIngs.GL2.CongruenceIndex
LeanPool.LeanModularForms.HeckeRIngs.GL2.Degree
LeanPool.LeanModularForms.HeckeRIngs.GL2.HeckeAction
LeanPool.LeanModularForms.HeckeRIngs.GL2.HeckeModularForm
LeanPool.LeanModularForms.HeckeRIngs.GL2.MultiplicationTable
LeanPool.LeanModularForms.HeckeRIngs.GLn.Basic
LeanPool.LeanModularForms.HeckeRIngs.GLn.CoprimeMul
LeanPool.LeanModularForms.HeckeRIngs.GLn.CosetDecomposition
LeanPool.LeanModularForms.HeckeRIngs.GLn.Degree
LeanPool.LeanModularForms.HeckeRIngs.GLn.DiagonalCosets
LeanPool.LeanModularForms.HeckeRIngs.GLn.PolynomialRing
LeanPool.LeanModularForms.HeckeRIngs.GLn.PrimeDecomposition
LeanPool.LeanModularForms.HeckeRIngs.GLn.SLnTransvection
LeanPool.LeanModularForms.HeckeRIngs.GLn.TransposeAntiInvolution
LeanPool.LeanModularForms.Modularforms.Generators.Defs
LeanPool.LeanModularForms.Modularforms.Generators.Injectivity
LeanPool.LeanModularForms.Modularforms.Generators.Surjectivity
LeanPool.LeanModularForms.ValenceFormula.Boundary.Basic
LeanPool.LeanModularForms.ValenceFormula.Boundary.Bounds
LeanPool.LeanModularForms.ValenceFormula.Boundary.Smooth
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.Basic
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.EndpointCorner
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.Main
LeanPool.LeanModularForms.ValenceFormula.PVChain.ArcContribution
LeanPool.LeanModularForms.ValenceFormula.PVChain.Assembly
LeanPool.LeanModularForms.ValenceFormula.PVChain.Helpers
LeanPool.LeanModularForms.ValenceFormula.PVChain.OnCurveCapture
LeanPool.LeanModularForms.ValenceFormula.PVChain.ResidueSideInfra
LeanPool.LeanModularForms.ValenceFormula.PVChain.Seg5CuspIntegral
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.AngleAnalysis
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopyDerivBounds
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopyDiff
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopySmooth
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.Geometry
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.HomotopyDef
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheorem
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheoremBound
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheoremDerivCont
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.PolygonProps
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.PolygonSlope
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.RadialHomotopy
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.WindingBase
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.WindingProof
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.Common
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.I
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.Rho
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.RhoPlusOne
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.BoundaryVanishing
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.CPVExistence
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.CutoffInfrastructure
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.HigherOrderAssembly
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.PerTermVanishing
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MultipointPV.DominatedConvergence
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.Framework
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.LeftEdge
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.RightEdge
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.UnitArc
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.UnitArcHelpers
LeanPool.LeanModularForms.ValenceFormula.PVChain.Assembly.ResidueSide
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.PerTermVanishing.CPVHelpers
Imported by