Documentation
SpherePacking
Search
return to top
source
Imports
Init
SpherePacking.Basic.E8
SpherePacking.Basic.PeriodicPacking
SpherePacking.Basic.SpherePacking
SpherePacking.CohnElkies.LPBound
SpherePacking.CohnElkies.Prereqs
SpherePacking.ForMathlib.Asymptotics
SpherePacking.ForMathlib.AtImInfty
SpherePacking.ForMathlib.Bornology
SpherePacking.ForMathlib.Cardinal
SpherePacking.ForMathlib.Dual
SpherePacking.ForMathlib.ENNReal
SpherePacking.ForMathlib.ENat
SpherePacking.ForMathlib.Encard
SpherePacking.ForMathlib.Finsupp
SpherePacking.ForMathlib.Fourier
SpherePacking.ForMathlib.FunctionsBoundedAtInfty
SpherePacking.ForMathlib.InnerProductSpace
SpherePacking.ForMathlib.InvPowSummability
SpherePacking.ForMathlib.Radial
SpherePacking.ForMathlib.RadialSchwartz
SpherePacking.ForMathlib.Real
SpherePacking.ForMathlib.SlashActions
SpherePacking.ForMathlib.SpecificLimits
SpherePacking.ForMathlib.UpperHalfPlane
SpherePacking.ForMathlib.Vec
SpherePacking.ForMathlib.VolumeOfBalls
SpherePacking.ForMathlib.ZLattice
SpherePacking.ForMathlib.tprod
SpherePacking.MagicFunction.PolyFourierCoeffBound
SpherePacking.ModularForms.AtImInfty
SpherePacking.ModularForms.BigO
SpherePacking.ModularForms.Cauchylems
SpherePacking.ModularForms.Delta
SpherePacking.ModularForms.E2
SpherePacking.ModularForms.Eisenstein
SpherePacking.ModularForms.Eisensteinqexpansions
SpherePacking.ModularForms.Icc_Ico_lems
SpherePacking.ModularForms.IsCuspForm
SpherePacking.ModularForms.JacobiTheta
SpherePacking.ModularForms.QExpansion
SpherePacking.ModularForms.SlashActionAuxil
SpherePacking.ModularForms.clog_arg_lems
SpherePacking.ModularForms.cotangent
SpherePacking.ModularForms.csqrt
SpherePacking.ModularForms.equivs
SpherePacking.ModularForms.eta
SpherePacking.ModularForms.exp_lems
SpherePacking.ModularForms.iteratedderivs
SpherePacking.ModularForms.limunder_lems
SpherePacking.ModularForms.logDeriv_lems
SpherePacking.ModularForms.multipliable_lems
SpherePacking.ModularForms.qExpansion_lems
SpherePacking.ModularForms.riemannZetalems
SpherePacking.ModularForms.summable_lems
SpherePacking.ModularForms.tendstolems
SpherePacking.ModularForms.tsumderivWithin
SpherePacking.ModularForms.uniformcts
SpherePacking.ModularForms.upperhalfplane
SpherePacking.Tactic.NormNumI
SpherePacking.Tactic.NormNumI_Scratch
SpherePacking.ForMathlib.CauchyGoursat.OpenRectangular
SpherePacking.ForMathlib.CauchyGoursat.Triangular
SpherePacking.MagicFunction.a.Basic
SpherePacking.MagicFunction.a.Schwartz
SpherePacking.Tactic.Test.AlphaEvolve_Matmul_Verification
SpherePacking.Tactic.Test.NormNumI
SpherePacking.MagicFunction.a.IntegralEstimates.I1
SpherePacking.MagicFunction.a.IntegralEstimates.I2
SpherePacking.MagicFunction.a.IntegralEstimates.I3
SpherePacking.MagicFunction.a.IntegralEstimates.I4
SpherePacking.MagicFunction.a.IntegralEstimates.I5
SpherePacking.MagicFunction.a.IntegralEstimates.I6
Imported by