Documentation
SpherePacking
Search
return to top
source
Imports
Init
SpherePacking.MainTheorem
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.ENNReal
SpherePacking.ForMathlib.ENat
SpherePacking.ForMathlib.Encard
SpherePacking.ForMathlib.Finsupp
SpherePacking.ForMathlib.Fourier
SpherePacking.ForMathlib.FunctionsBoundedAtInfty
SpherePacking.ForMathlib.InnerProductSpace
SpherePacking.ForMathlib.InvPowSummability
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.IntegralParametrisations
SpherePacking.MagicFunction.PolyFourierCoeffBound
SpherePacking.ModularForms.AtImInfty
SpherePacking.ModularForms.BigO
SpherePacking.ModularForms.Cauchylems
SpherePacking.ModularForms.Delta
SpherePacking.ModularForms.Derivative
SpherePacking.ModularForms.DimensionFormulas
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.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.PoissonSummation.DualLattice
SpherePacking.ForMathlib.PoissonSummation.EuclideanSpace
SpherePacking.ForMathlib.PoissonSummation.Lattice_Equiv
SpherePacking.ForMathlib.PoissonSummation.SchwartzMap
SpherePacking.ForMathlib.PoissonSummation.Zn_Pi
SpherePacking.ForMathlib.PoissonSummation.Zn_to_Euclidean
SpherePacking.ForMathlib.RadialSchwartz.Multidimensional
SpherePacking.MagicFunction.a.Basic
SpherePacking.MagicFunction.a.Eigenfunction
SpherePacking.MagicFunction.a.Schwartz
SpherePacking.MagicFunction.a.SpecialValues
SpherePacking.MagicFunction.b.Basic
SpherePacking.MagicFunction.b.Eigenfunction
SpherePacking.MagicFunction.b.Schwartz
SpherePacking.MagicFunction.b.SpecialValues
SpherePacking.MagicFunction.b.psi
SpherePacking.MagicFunction.g.Basic
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