forked from thefundamentaltheor3m/Sphere-Packing-Lean
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathSpherePacking.lean
More file actions
84 lines (84 loc) · 3.88 KB
/
SpherePacking.lean
File metadata and controls
84 lines (84 loc) · 3.88 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
import SpherePacking.Basic.E8
import SpherePacking.Basic.PeriodicPacking
import SpherePacking.Basic.SpherePacking
import SpherePacking.CohnElkies.LPBound
import SpherePacking.CohnElkies.Prereqs
import SpherePacking.ForMathlib.Asymptotics
import SpherePacking.ForMathlib.AtImInfty
import SpherePacking.ForMathlib.Cardinal
import SpherePacking.ForMathlib.CauchyGoursat.OpenRectangular
import SpherePacking.ForMathlib.ENNReal
import SpherePacking.ForMathlib.ENat
import SpherePacking.ForMathlib.Encard
import SpherePacking.ForMathlib.Finsupp
import SpherePacking.ForMathlib.Fourier
import SpherePacking.ForMathlib.FunctionsBoundedAtInfty
import SpherePacking.ForMathlib.InnerProductSpace
import SpherePacking.ForMathlib.InvPowSummability
import SpherePacking.ForMathlib.PoissonSummation.DualLattice
import SpherePacking.ForMathlib.PoissonSummation.EuclideanSpace
import SpherePacking.ForMathlib.PoissonSummation.Lattice_Equiv
import SpherePacking.ForMathlib.PoissonSummation.SchwartzMap
import SpherePacking.ForMathlib.PoissonSummation.Zn_Pi
import SpherePacking.ForMathlib.PoissonSummation.Zn_to_Euclidean
import SpherePacking.ForMathlib.RadialSchwartz.Multidimensional
import SpherePacking.ForMathlib.Real
import SpherePacking.ForMathlib.SlashActions
import SpherePacking.ForMathlib.SpecificLimits
import SpherePacking.ForMathlib.UpperHalfPlane
import SpherePacking.ForMathlib.Vec
import SpherePacking.ForMathlib.VolumeOfBalls
import SpherePacking.ForMathlib.ZLattice
import SpherePacking.ForMathlib.tprod
import SpherePacking.MagicFunction.IntegralParametrisations
import SpherePacking.MagicFunction.PolyFourierCoeffBound
import SpherePacking.MagicFunction.a.Basic
import SpherePacking.MagicFunction.a.Eigenfunction
import SpherePacking.MagicFunction.a.IntegralEstimates.I1
import SpherePacking.MagicFunction.a.IntegralEstimates.I2
import SpherePacking.MagicFunction.a.IntegralEstimates.I3
import SpherePacking.MagicFunction.a.IntegralEstimates.I4
import SpherePacking.MagicFunction.a.IntegralEstimates.I5
import SpherePacking.MagicFunction.a.IntegralEstimates.I6
import SpherePacking.MagicFunction.a.Schwartz
import SpherePacking.MagicFunction.a.SpecialValues
import SpherePacking.MagicFunction.b.Basic
import SpherePacking.MagicFunction.b.Eigenfunction
import SpherePacking.MagicFunction.b.Schwartz
import SpherePacking.MagicFunction.b.SpecialValues
import SpherePacking.MagicFunction.b.psi
import SpherePacking.MagicFunction.g.Basic
import SpherePacking.MainTheorem
import SpherePacking.ModularForms.AtImInfty
import SpherePacking.ModularForms.BigO
import SpherePacking.ModularForms.Cauchylems
import SpherePacking.ModularForms.Delta
import SpherePacking.ModularForms.Derivative
import SpherePacking.ModularForms.DimensionFormulas
import SpherePacking.ModularForms.E2
import SpherePacking.ModularForms.Eisenstein
import SpherePacking.ModularForms.Eisensteinqexpansions
import SpherePacking.ModularForms.Icc_Ico_lems
import SpherePacking.ModularForms.IsCuspForm
import SpherePacking.ModularForms.JacobiTheta
import SpherePacking.ModularForms.QExpansion
import SpherePacking.ModularForms.SlashActionAuxil
import SpherePacking.ModularForms.clog_arg_lems
import SpherePacking.ModularForms.csqrt
import SpherePacking.ModularForms.equivs
import SpherePacking.ModularForms.eta
import SpherePacking.ModularForms.exp_lems
import SpherePacking.ModularForms.iteratedderivs
import SpherePacking.ModularForms.limunder_lems
import SpherePacking.ModularForms.logDeriv_lems
import SpherePacking.ModularForms.multipliable_lems
import SpherePacking.ModularForms.qExpansion_lems
import SpherePacking.ModularForms.riemannZetalems
import SpherePacking.ModularForms.summable_lems
import SpherePacking.ModularForms.tendstolems
import SpherePacking.ModularForms.tsumderivWithin
import SpherePacking.ModularForms.uniformcts
import SpherePacking.ModularForms.upperhalfplane
import SpherePacking.Tactic.NormNumI
import SpherePacking.Tactic.NormNumI_Scratch
import SpherePacking.Tactic.Test.NormNumI