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
92 lines (91 loc) · 4.79 KB
/
SpherePacking.lean
File metadata and controls
92 lines (91 loc) · 4.79 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
85
86
87
88
89
90
91
92
module -- shake: keep-all
public import SpherePacking.Basic.E8
public import SpherePacking.Basic.PeriodicPacking
public import SpherePacking.Basic.SpherePacking
public import SpherePacking.CohnElkies.LPBound
public import SpherePacking.CohnElkies.Prereqs
public import SpherePacking.ForMathlib.Asymptotics
public import SpherePacking.ForMathlib.AtImInfty
public import SpherePacking.ForMathlib.Cardinal
public import SpherePacking.ForMathlib.CauchyGoursat.OpenRectangular
public import SpherePacking.ForMathlib.Cusps
public import SpherePacking.ForMathlib.ENNReal
public import SpherePacking.ForMathlib.ENat
public import SpherePacking.ForMathlib.Encard
public import SpherePacking.ForMathlib.Finsupp
public import SpherePacking.ForMathlib.Fourier
public import SpherePacking.ForMathlib.FunctionsBoundedAtInfty
public import SpherePacking.ForMathlib.InnerProductSpace
public import SpherePacking.ForMathlib.InvPowSummability
public import SpherePacking.ForMathlib.MDifferentiableFunProp
public import SpherePacking.ForMathlib.RadialSchwartz.Multidimensional
public import SpherePacking.ForMathlib.Real
public import SpherePacking.ForMathlib.SlashActions
public import SpherePacking.ForMathlib.SpecificLimits
public import SpherePacking.ForMathlib.UpperHalfPlane
public import SpherePacking.ForMathlib.Vec
public import SpherePacking.ForMathlib.VolumeOfBalls
public import SpherePacking.ForMathlib.ZLattice
public import SpherePacking.ForMathlib.tprod
public import SpherePacking.MagicFunction.IntegralParametrisations
public import SpherePacking.MagicFunction.PolyFourierCoeffBound
public import SpherePacking.MagicFunction.a.Basic
public import SpherePacking.MagicFunction.a.Eigenfunction
public import SpherePacking.MagicFunction.a.Integrability.ComplexIntegrands
public import SpherePacking.MagicFunction.a.Integrability.Integrability
public import SpherePacking.MagicFunction.a.Integrability.RealIntegrands
public import SpherePacking.MagicFunction.a.IntegralEstimates.I1
public import SpherePacking.MagicFunction.a.IntegralEstimates.I2
public import SpherePacking.MagicFunction.a.IntegralEstimates.I3
public import SpherePacking.MagicFunction.a.IntegralEstimates.I4
public import SpherePacking.MagicFunction.a.IntegralEstimates.I5
public import SpherePacking.MagicFunction.a.IntegralEstimates.I6
public import SpherePacking.MagicFunction.a.Schwartz
public import SpherePacking.MagicFunction.a.SpecialValues
public import SpherePacking.MagicFunction.b.Basic
public import SpherePacking.MagicFunction.b.Eigenfunction
public import SpherePacking.MagicFunction.b.Schwartz
public import SpherePacking.MagicFunction.b.SpecialValues
public import SpherePacking.MagicFunction.b.psi
public import SpherePacking.MagicFunction.g.Basic
public import SpherePacking.MainTheorem
public import SpherePacking.ModularForms.BigO
public import SpherePacking.ModularForms.Cauchylems
public import SpherePacking.ModularForms.Delta
public import SpherePacking.ModularForms.Derivative
public import SpherePacking.ModularForms.DimensionFormulas
public import SpherePacking.ModularForms.E2
public import SpherePacking.ModularForms.Eisenstein
public import SpherePacking.ModularForms.EisensteinAsymptotics
public import SpherePacking.ModularForms.Eisensteinqexpansions
public import SpherePacking.ModularForms.FG
public import SpherePacking.ModularForms.Icc_Ico_lems
public import SpherePacking.ModularForms.IsCuspForm
public import SpherePacking.ModularForms.JacobiTheta
public import SpherePacking.ModularForms.PhiTransform
public import SpherePacking.ModularForms.QExpansion
public import SpherePacking.ModularForms.RamanujanIdentities
public import SpherePacking.ModularForms.ResToImagAxis
public import SpherePacking.ModularForms.SerreDerivativeSlash
public import SpherePacking.ModularForms.SlashActionAuxil
public import SpherePacking.ModularForms.ThetaDerivIdentities
public import SpherePacking.ModularForms.clog_arg_lems
public import SpherePacking.ModularForms.csqrt
public import SpherePacking.ModularForms.equivs
public import SpherePacking.ModularForms.eta
public import SpherePacking.ModularForms.exp_lems
public import SpherePacking.ModularForms.iteratedderivs
public import SpherePacking.ModularForms.limunder_lems
public import SpherePacking.ModularForms.multipliable_lems
public import SpherePacking.ModularForms.qExpansion_lems
public import SpherePacking.ModularForms.riemannZetalems
public import SpherePacking.ModularForms.summable_lems
public import SpherePacking.ModularForms.tendstolems
public import SpherePacking.ModularForms.tsumderivWithin
public import SpherePacking.ModularForms.uniformcts
public import SpherePacking.ModularForms.upperhalfplane
public import SpherePacking.Tactic.NormNumI
public import SpherePacking.Tactic.NormNumI_Scratch
public import SpherePacking.Tactic.TendstoCont
public import SpherePacking.Tactic.Test.NormNumI
public import SpherePacking.Tactic.Test.TendstoCont