SpherePacking.lean

import SpherePacking.Basic.Domains.RightHalfPlane
import SpherePacking.Basic.Domains.WedgeSet
import SpherePacking.Basic.PeriodicPacking.Aux
import SpherePacking.Basic.PeriodicPacking.BoundaryControl
import SpherePacking.Basic.PeriodicPacking.DensityFormula
import SpherePacking.Basic.PeriodicPacking.PeriodicConstant
import SpherePacking.Basic.PeriodicPacking.Theorem22
import SpherePacking.Basic.SpherePacking
import SpherePacking.CohnElkies.DualSubmoduleDiscrete
import SpherePacking.CohnElkies.EqualityCaseCommute
import SpherePacking.CohnElkies.EqualityCaseVanishing
import SpherePacking.CohnElkies.LPBound
import SpherePacking.CohnElkies.LPBoundAux
import SpherePacking.CohnElkies.LPBoundCalcLemmas
import SpherePacking.CohnElkies.LPBoundReindex
import SpherePacking.CohnElkies.LPBoundSummability
import SpherePacking.CohnElkies.LPBoundSwapSums
import SpherePacking.CohnElkies.LatticeSumBounds
import SpherePacking.CohnElkies.PoissonSummationGeneral
import SpherePacking.CohnElkies.PoissonSummationLattices.PoissonSummation
import SpherePacking.CohnElkies.PoissonSummationLattices.UnitAddTorus
import SpherePacking.CohnElkies.PoissonSummationSchwartz.Basic
import SpherePacking.CohnElkies.PoissonSummationSchwartz.PoissonSummation
import SpherePacking.CohnElkies.Prereqs
import SpherePacking.Contour.GaussianIntegral
import SpherePacking.Contour.MobiusInv.Basic
import SpherePacking.Contour.MobiusInv.ContourChange
import SpherePacking.Contour.MobiusInv.LineMap
import SpherePacking.Contour.MobiusInv.PermJ12PsiFourier
import SpherePacking.Contour.MobiusInv.Segments
import SpherePacking.Contour.MobiusInv.WedgeSet
import SpherePacking.Contour.MobiusInv.WedgeSetContour
import SpherePacking.Contour.PermJ12Contour
import SpherePacking.Contour.PermJ12CurveIntegral
import SpherePacking.Contour.PermJ12DiffContOnCl
import SpherePacking.Contour.PermJ12Fourier
import SpherePacking.Contour.PermJ12FourierCurveIntegral
import SpherePacking.Contour.PermJ12Tendsto
import SpherePacking.Contour.PermJ5Kernel
import SpherePacking.Contour.Segments
import SpherePacking.Dim24.Inequalities.AppendixA.AbsBoundQ
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingCoeffs
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingDeltaBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingKernelRewrite
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.BleadingNumDecomp
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.CoeffBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.CoeffMatchingComputations
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.CoeffMatchingLemmas
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.CoeffQTableRewrites
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.CoeffZModel
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.ConstBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.ConvolutionAlgebra
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.DeltaCoeffBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.DeltaHatSqTable
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.EvenReindex
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.FinalLowerBound
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.HeadEqualsExactTrunc
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.LowerBound
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.Numerators
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.Phi1CoreTable
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.Phi2CoreTable
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PhiCoeffBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PhiDeltaQSeries.Basic
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PhiDeltaQSeries.Identities
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PiBoundsAndTruncCompare
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PowerBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiCoeffFunAndTail.Basic
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiCoeffFunAndTail.PsiCoeffFun
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiCoeffMatch
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiRSeriesSetup.Basic
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiRSeriesSetup.Defs
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiRSeriesSetup.SparseCoeffs
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.PsiTable
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.QSeriesHelpers
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.QSeriesTailAndCoeffBounds.TailBound
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.RemainderBound
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.SeriesSplit
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.ShiftSums
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.TailBounds
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.ThetaRSeriesSpecialize
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.TruncCoeffCertificate
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.VarphiQSeries
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.VarphiTable
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingNumLowerBound.ZVArith
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingTailReduction
import SpherePacking.Dim24.Inequalities.AppendixA.BLeadingTruncBounds
import SpherePacking.Dim24.Inequalities.AppendixA.CoeffBoundConstants
import SpherePacking.Dim24.Inequalities.AppendixA.Constants
import SpherePacking.Dim24.Inequalities.AppendixA.EisensteinSeriesBounds
import SpherePacking.Dim24.Inequalities.AppendixA.ExpBounds
import SpherePacking.Dim24.Inequalities.AppendixA.GeometricTailBounds
import SpherePacking.Dim24.Inequalities.AppendixA.Ineq2TruncLeOneCoeffsRigor
import SpherePacking.Dim24.Inequalities.AppendixA.PolyOfCoeffsLemmas
import SpherePacking.Dim24.Inequalities.AppendixA.Polynomials.Basic
import SpherePacking.Dim24.Inequalities.AppendixA.Polynomials.CoeffsBleading
import SpherePacking.Dim24.Inequalities.AppendixA.Polynomials.CoeffsIneq2
import SpherePacking.Dim24.Inequalities.AppendixA.Polynomials.CoeffsVarphi
import SpherePacking.Dim24.Inequalities.AppendixA.Polynomials.CoeffsVarphiInt
import SpherePacking.Dim24.Inequalities.AppendixA.PsiInumCoeffsTable
import SpherePacking.Dim24.Inequalities.AppendixA.QSeries
import SpherePacking.Dim24.Inequalities.AppendixA.QSeriesMul
import SpherePacking.Dim24.Inequalities.AppendixA.QSeriesSummable
import SpherePacking.Dim24.Inequalities.AppendixA.QSeriesTailBounds
import SpherePacking.Dim24.Inequalities.AppendixA.RBounds
import SpherePacking.Dim24.Inequalities.AppendixA.RSeriesTailBounds
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.CoeffModel
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.ExactTruncTail.AuxIneqs
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.ExactTruncTail.ExactTruncation
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.HeadIdentification
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.TailBound.NormRemainder
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.TailBound.PowComparisons
import SpherePacking.Dim24.Inequalities.AppendixA.VarphiLeOneNumLowerBound.TailBound.TailEstimate
import SpherePacking.Dim24.Inequalities.BLeadingTerms
import SpherePacking.Dim24.Inequalities.Certificate.ZVArith
import SpherePacking.Dim24.Inequalities.Defs
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.AppendixA.Trunc
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.AppendixA.TruncPos
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.DenomReduction.LowerBound
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.DenomReduction.Numerators
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2PsiSnum.PsiSnumCoeffs.Bounds
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2PsiSnum.PsiSnumCoeffs.Cert
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2PsiSnum.RSeries
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2PsiSnum.RSeriesOps
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2PsiSnum.SummabilityReindex
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2Varphi.CertAssemble
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2Varphi.CertData
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2Varphi.CertPrelude
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Ineq2Varphi.TailBound
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.Monotonicity
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.NumTruncBound
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.TailNumerics.ConstantsPi
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.TailNumerics.GeomRatio
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.TailNumerics.Majorant
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.TruncEvalRewrite
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.TruncRewrite
import SpherePacking.Dim24.Inequalities.Ineq2.GeOne.VarphiRealPart
import SpherePacking.Dim24.Inequalities.Ineq2.GeOneCoeffs
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumCert.SumRange
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumCert.VerifyH4H2
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumCert.VerifyThetaH4
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumOps
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumTables.H4Pow2Table
import SpherePacking.Dim24.Inequalities.Ineq2.GeOnePsiSnumTables.ThetaTables
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.Positivity
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.Trunc
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.CoeffModel
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.Denom
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTrunc
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.Common
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.LargeDefs
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.LargeEvalLe
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.LargeEvalPos
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.SmallDefs
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.SmallEvalLe
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.ExactTruncPosRigorous.SmallIntervalLB
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.Defs
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.Head
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.TailConstants
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.TailNormBound
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.TailTermBounds
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.NumTailBound.TailTriangle
import SpherePacking.Dim24.Inequalities.Ineq2.LeOne.TruncAux.PariCoeffs
import SpherePacking.Dim24.Inequalities.Ineq2.Statement
import SpherePacking.Dim24.Inequalities.VarphiNeg.GeOne.AppendixABridge
import SpherePacking.Dim24.Inequalities.VarphiNeg.GeOne.Defs
import SpherePacking.Dim24.Inequalities.VarphiNeg.GeOne.Negativity
import SpherePacking.Dim24.Inequalities.VarphiNeg.GeOne.TailBound.Geometric
import SpherePacking.Dim24.Inequalities.VarphiNeg.GeOne.TailBound.TailBound
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Negativity
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Transform
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.DeltaBounds
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.ExactTruncPosRigorous.Positivity
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.ExactTruncPosRigorous.Prelude
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.ExactTruncPosRigorous.Term2LowerBound
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.ExactTruncPosRigorous.Term4LowerBound
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.ExactTruncTailBound
import SpherePacking.Dim24.Inequalities.VarphiNeg.LeOne.Trunc.TransformedRe
import SpherePacking.Dim24.Inequalities.VarphiNeg.Statement
import SpherePacking.Dim24.LeechLattice.Basis
import SpherePacking.Dim24.LeechLattice.Defs
import SpherePacking.Dim24.LeechLattice.Instances
import SpherePacking.Dim24.LeechLattice.Norm
import SpherePacking.Dim24.MagicFunction.A.Defs
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Prelude
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.Function
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I1Decay
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I1Prelude
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I1Smoothness
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I2Smooth
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I3Smooth
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I4Smooth
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I5Smooth
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I6ContDiffDecay
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I6Differentiation
import SpherePacking.Dim24.MagicFunction.A.DefsAux.Schwartz.I6Preamble
import SpherePacking.Dim24.MagicFunction.A.DefsAux.VarphiExpBounds
import SpherePacking.Dim24.MagicFunction.A.Eigen.Eigenfunction
import SpherePacking.Dim24.MagicFunction.A.Eigen.GaussianFourier
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12ContourDeformation
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12CurveIntegrals
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12FourierCurveIntegrals
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12FourierKernels
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12Integrability
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12Measurability
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12Prelude
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12ProductIntegrability
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI12Regularity
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI56ChangeOfVariables
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI56FourierPermutation
import SpherePacking.Dim24.MagicFunction.A.Eigen.PermI56KernelSetup
import SpherePacking.Dim24.MagicFunction.A.Eigen.Prelude
import SpherePacking.Dim24.MagicFunction.A.LaplaceZeros
import SpherePacking.Dim24.MagicFunction.A.LaplaceZerosTail.HolomorphyHelpers
import SpherePacking.Dim24.MagicFunction.A.LaplaceZerosTail.TailBounds
import SpherePacking.Dim24.MagicFunction.A.LaplaceZerosTail.TailDeform
import SpherePacking.Dim24.MagicFunction.A.PureImag
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Aux01
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Aux02
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Aux03.Integrability
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Aux03.Transforms
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Aux04
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.EvenAProfile.AtFour
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.EvenAProfile.Basic
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivDefs
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivFour
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoAtTwo
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesBridge
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesConvergentRange
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesEqAvaluesImpl
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesRemIntDom
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesRemainderIntegral
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesRemainderIntegralDCT
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesRemainderIntegralDefs
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.AvaluesRemainderLargeBound
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Basic
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.CCancel
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.CancelD
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.CoeffExp
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Defs
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.LaplaceIntegrals
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Ptilde
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.SincAux
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.SincExp
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.SingularIntegral
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Varphi2ConstCoeff
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Varphi2ConstTerm
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.DerivTwoLaurent.Varphi2ConstValue
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Final.Values
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Prelude
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Radial
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Varphi1A
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Varphi1B
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Varphi1C
import SpherePacking.Dim24.MagicFunction.A.SpecialValues.Varphi2
import SpherePacking.Dim24.MagicFunction.A.VarphiBounds
import SpherePacking.Dim24.MagicFunction.A.Zeros.ContourIdentities
import SpherePacking.Dim24.MagicFunction.A.Zeros.DoubleZeros
import SpherePacking.Dim24.MagicFunction.B.Defs.Eigenfunction
import SpherePacking.Dim24.MagicFunction.B.Defs.J1Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.J1SmoothDecay
import SpherePacking.Dim24.MagicFunction.B.Defs.J1SmoothIntegrals
import SpherePacking.Dim24.MagicFunction.B.Defs.J2Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.J3Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.J4Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.J5Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.J5SmoothIntegrals
import SpherePacking.Dim24.MagicFunction.B.Defs.J6Derivatives
import SpherePacking.Dim24.MagicFunction.B.Defs.J6Smooth
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiExtensions
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiSDecay
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiSPrelims
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiSRectAnalytic
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiSRectIdentity
import SpherePacking.Dim24.MagicFunction.B.Defs.PsiSlash
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12ContourIdentity
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12CurveIntegrals
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12DiffContOnCl
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12FourierJ1
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12FourierJ2
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12Measurability
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ12Regularity
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ5
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ5ChangeOfVariables
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ5Integrability
import SpherePacking.Dim24.MagicFunction.B.Eigen.PermJ5KernelSetup
import SpherePacking.Dim24.MagicFunction.B.Eigen.Prelude
import SpherePacking.Dim24.MagicFunction.B.PureImag
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Basic
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.BProfileDeriv
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.BfunFour
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.BfunTwo
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.CuspAtInfinity
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.CuspCoefficient.H2
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.CuspCoefficient.H4
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.CuspCoefficient.PsiI
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.DeltaQHalf.Base
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.DeltaQHalf.InvSq
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.H2H4.H2
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.H2H4.H4
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.QHalfTheta4
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.Rectangle
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.Theta2Trunc
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.TopEdge.Base
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.TopEdge.J6
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Derivatives.TopEdge.Limits
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.EvenU.BProfileZeros
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.EvenU.J135Factor
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.EvenU.SumIdentities
import SpherePacking.Dim24.MagicFunction.B.SpecialValues.Final
import SpherePacking.Dim24.MagicFunction.B.Zeros
import SpherePacking.Dim24.MagicFunction.F.BKernelAsymptotics
import SpherePacking.Dim24.MagicFunction.F.Constants
import SpherePacking.Dim24.MagicFunction.F.Defs
import SpherePacking.Dim24.MagicFunction.F.Fourier
import SpherePacking.Dim24.MagicFunction.F.Laplace.A.Basic
import SpherePacking.Dim24.MagicFunction.F.Laplace.Apply
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.Basic
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.LeadingCorrection
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingBounds.BKernelSubLeadingBound
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingBounds.DeltaDivQLowerBound
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingBounds.ExactTruncBound
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingContinuation.Agreement
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingContinuation.Analyticity
import SpherePacking.Dim24.MagicFunction.F.Laplace.B.SubLeadingContinuation.TailIntegrand
import SpherePacking.Dim24.MagicFunction.F.Laplace.Equality.A.AKernelIntegralIdentity
import SpherePacking.Dim24.MagicFunction.F.Laplace.Equality.A.Defs
import SpherePacking.Dim24.MagicFunction.F.Laplace.Equality.A.GPsiIntegrability
import SpherePacking.Dim24.MagicFunction.F.Laplace.Equality.A.GVIntegralDecomposition
import SpherePacking.Dim24.MagicFunction.F.Laplace.Equality.B
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.B
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.BSubLeading
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Basic
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.BKernelBounds
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.Continuation
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.Differentiable
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.IntegrandSetup
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.LaplaceSplit
import SpherePacking.Dim24.MagicFunction.F.Laplace.Fourier.Continuation.Prelude
import SpherePacking.Dim24.MagicFunction.F.Laplace.KernelTools
import SpherePacking.Dim24.MagicFunction.F.Laplace.Kernels
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.AProfile
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.BProfile.Bounds
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.BProfile.IntegralLemmas
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.BProfile.LaplaceFormula
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.BProfile.RectangleIdentity
import SpherePacking.Dim24.MagicFunction.F.Laplace.Profiles.BProfile.TailDifference
import SpherePacking.Dim24.MagicFunction.F.Laplace.TopologyDomains
import SpherePacking.Dim24.MagicFunction.F.ProfileComplex.A1
import SpherePacking.Dim24.MagicFunction.F.ProfileComplex.A2
import SpherePacking.Dim24.MagicFunction.F.ProfileComplex.A3
import SpherePacking.Dim24.MagicFunction.F.ProfileComplex.B
import SpherePacking.Dim24.MagicFunction.F.RealValued
import SpherePacking.Dim24.MagicFunction.F.Scaled
import SpherePacking.Dim24.MagicFunction.F.Sign.Aux
import SpherePacking.Dim24.MagicFunction.F.Sign.SignConditions
import SpherePacking.Dim24.MagicFunction.F.SpecialValues
import SpherePacking.Dim24.MagicFunction.F.UpperBound
import SpherePacking.Dim24.MagicFunction.F.Zero
import SpherePacking.Dim24.MagicFunction.MkRadial
import SpherePacking.Dim24.MagicFunction.PureImagCommon
import SpherePacking.Dim24.MagicFunction.Radial
import SpherePacking.Dim24.MagicFunction.SpecialValuesExpU
import SpherePacking.Dim24.MainTheorem
import SpherePacking.Dim24.ModularForms.Psi.Defs
import SpherePacking.Dim24.ModularForms.Psi.ImagAxis
import SpherePacking.Dim24.ModularForms.Psi.Relations
import SpherePacking.Dim24.ModularForms.Varphi
import SpherePacking.Dim24.Packing
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Biplane23632
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.BiplaneBasic
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.BiplaneParams
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Defs
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.DerivedS3622
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Design23632Forced
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Design23632Unique
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Design23632VertexFamilies
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.DotBilin
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.DotSupportLite
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayBounds
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayConcrete
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayDefs
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.Determine
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.OctadInterNumbers
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.OctadInterPairs
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.OctadInterSums
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.OctadIntersections
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.OctadsEq
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.Span
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctads.WordFinset
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.CodeFromOctadsAux
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.Uniqueness
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.Weight8Count
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.GolayUniqueness.Weight8CountAux
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.LinearCode
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.Orthogonality
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerDefs
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerDerived
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerLambda
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerParams
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerS3622.Classify.PermuteInvariants
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.SteinerS3622.PermuteFix01
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneFromSharp.Blocks
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneFromSharp.EvenBasis
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneFromSharp.ExistsStructure
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneFromSharp.Lifts
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneIso
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneUniqueness.ChooseB0
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneUniqueness.Extract
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneUniqueness.PairIdx
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.BiplaneUniqueness.Relabel
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ClassicalWitt.BlockInter
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ClassicalWitt.CodeFromDes
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ClassicalWitt.DesignCodeCard
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ClassicalWitt.SharpInput
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ClassicalWitt.Uniqueness
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.DesignUniqueness
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.DodecadExists
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.EvenBasisSpan
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.PunctureEven
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.ReconstructedCanonBiplane
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpGolayAux.Extraction
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpGolayAux.Generators
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpGolayAux.Span
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpGolayAux.Transport
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpGolayUniqueFromBiplane
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.SharpInput
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.Step4.Aux
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.Step4.Step4Iso
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.Step4.Step4VertexFamilies
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.Step4.VFsClassify
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittDesignUniqueTheory.Step4.VertexFamilyClassify
import SpherePacking.Dim24.Uniqueness.BS81.CodingTheory.WittParams
import SpherePacking.Dim24.Uniqueness.BS81.Defs
import SpherePacking.Dim24.Uniqueness.BS81.EqCase24Facts
import SpherePacking.Dim24.Uniqueness.BS81.EqCase24Integral
import SpherePacking.Dim24.Uniqueness.BS81.EqCase24Support
import SpherePacking.Dim24.Uniqueness.BS81.FromKissing
import SpherePacking.Dim24.Uniqueness.BS81.KissingUniqueness
import SpherePacking.Dim24.Uniqueness.BS81.LP.Delsarte
import SpherePacking.Dim24.Uniqueness.BS81.LP.F24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheorem.HarmPolyRecurrence24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheorem.ZonalPolynomial24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheoremFixed.GegenbauerBridge24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheoremFixed.HarmonicProjection24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheoremFixed.HarmonicProjection24Harm
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheoremFixed.HarmonicProjection24Proj
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.AdditionTheoremFixed.ZonalPolynomial24
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.Defs
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.DualCertificate
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.F24Coefficients
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.Kernel
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.KernelPSD
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.NormalizedRecurrence
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.Adjoint
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.AdjointOpsFixed
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.FiniteDimensional
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.Fischer
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.FischerDecompositionFixed
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.Harmonic
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.LaplacianLinPow
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.LaplacianR2PowLinPow
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.LinOps
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.R2AdjointFixed
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.PSD.R2Laplacian
import SpherePacking.Dim24.Uniqueness.BS81.LP.Gegenbauer24.ZonalKernelPSD
import SpherePacking.Dim24.Uniqueness.BS81.LP.Thm13Certificate
import SpherePacking.Dim24.Uniqueness.BS81.LatticeL
import SpherePacking.Dim24.Uniqueness.BS81.LatticeLIntegral
import SpherePacking.Dim24.Uniqueness.BS81.LatticeLShell4
import SpherePacking.Dim24.Uniqueness.BS81.Thm13.LPBound
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.AvgLemmas24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.BS81ToHarmonic24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.Bridge.HarmonicMeanZero24Gauss
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.DesignEquivBridge24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.DoubleSumsToHarmonics24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.EvalLemmas24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.FischerReduction24.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.FischerReduction24.Deg0Const
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.FischerReduction24.Deg1Harm
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.FischerReduction24.MulR2Pointwise
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.FischerReduction24.MulR2SphereAvg
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.HarmPolyRecurrence24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.IntegrableEvalPk24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.MeanZeroHarmonics24.AtZero
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.MeanZeroHarmonics24.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.AdditionTheorem.MeanZeroHarmonics24.MeanValue
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.Aux
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.AvgEquality
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.IndPoly
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.Moments.Core
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.Moments.IndPoly
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.CommonNeighbors44.SumEqualsCount
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.Defs
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.Design11.OddDegree
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.DesignEquiv
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.FromSharpness
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.InnerMvPoly24
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.MvPolyEval24Deriv
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.SphereAvg24Lemmas
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.SphereAvgFourthMoment24Final
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.SphereAvgInnerMoments24Final
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Design.SphereAvgMoments
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.DistanceDistribution.Defs
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.DistanceDistribution.DeriveEq11FromMomentsFinal
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.DistanceDistribution.FromSharpness
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Package
import SpherePacking.Dim24.Uniqueness.BS81.Thm14.Slack
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Dn.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Dn.Lemma18Count
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Dn.MinVec
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.Counts
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.HalfInteger
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.MinNorm
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.MomentIdentities
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.Solve
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma16.SphereAvgMoments24.Inner
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma17.Bound
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma17.InnerProducts
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma17.Shell4
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma18.Count44
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma19.ContainsD3
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma20.Base
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma20.ContainsDn
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma20.Defs
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma20.Step
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma20.StepMinVec
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeBounds.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeBounds.ReducedWitness
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeBounds.WeightLowerBound
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeCardBound
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeFromLattice
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.CodeMinDist
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Coordinates
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.IntegerCoords
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Isometry.CodeIsGolayCountFinal
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Isometry.GolayOctadGeneration
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Isometry.Types
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.LeechIsometry
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.LeechKissingSpan
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Patterns
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.ScaledCoord
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.Aux
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.BasepointInjection
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.BasepointTightness
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.Basic
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.Bridge
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.CodeFromLatticeDiff
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.DnFrameGauge
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.GaugeFix
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechConstructionA
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechConstructionAFourD24
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechConstructionALiftParity
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechConstructionAMain
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechD24
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechMembershipDefs
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechMembershipTypeI
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechMembershipTypeII
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechMembershipTypeIII
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4.LeechParityCode
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.Shell4Constraints
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Lemma21.ShellToLeechLattice
import SpherePacking.Dim24.Uniqueness.BS81.Thm15.Uniqueness
import SpherePacking.Dim24.Uniqueness.Defs
import SpherePacking.Dim24.Uniqueness.DistanceSpectrum.Reduction
import SpherePacking.Dim24.Uniqueness.Input.EqualityCase
import SpherePacking.Dim24.Uniqueness.Input.Roots
import SpherePacking.Dim24.Uniqueness.LatticeInvariants
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.ContactSet
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.Defs
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.EqualityCase
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.GlobalRigidity
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.Kissing.Normalize
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.LocalRigidity
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CE.Rigidity
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.CenterInner
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Cosets
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Discriminant
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.DiscriminantNondegenerate
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.DiscriminantPairing
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.DualCovolume
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.DualLatticeFinite
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.Discrete
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.FiniteShells
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.FundamentalDomain
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.MinNorm
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.ThetaAnalytic
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.ThetaSeries
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.EvenUnimodular.ThetaTransform
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.IsotropicBound
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.DualSelf
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.FullRank.InfiniteVolume
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.FullRank.OrthogonalDecomp
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.FullRank.UnimodularIsZLattice
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.IsZLatticeOfUnimodular
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.LatticeInSpan
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.ExtremalCoeffTwo
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.LeechMinShellSpan
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.MinShell
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.QExpansionCoeffTwo
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.ThetaEquality
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.ThetaExtremal
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.RootlessCase.ThetaMF
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.Setup
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Niemeier.ThetaUpperHalfPlane
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Overlattice.Basic
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Overlattice.CentersIsotropic
import SpherePacking.Dim24.Uniqueness.Rigidity.Classify.Overlattice.IndexCovolume
import SpherePacking.Dim24.Uniqueness.Rigidity.DensityProps
import SpherePacking.Dim24.Uniqueness.Rigidity.DualProps
import SpherePacking.Dim24.Uniqueness.Rigidity.Lemmas
import SpherePacking.Dim24.Uniqueness.Scale
import SpherePacking.Dim8.E8.Basic
import SpherePacking.Dim8.E8.Packing
import SpherePacking.Dim8.MagicFunction.a.Basic
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.FourierPermutations
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12ContourAux
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12ContourMain
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12Fourier
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12FourierAux
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12FourierIntegrableI1
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12FourierIntegrableI2
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12FourierMain
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12Prelude
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI12WedgeDomain
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI5Integrability
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI5Kernel
import SpherePacking.Dim8.MagicFunction.a.Eigenfunction.PermI5Main
import SpherePacking.Dim8.MagicFunction.a.Integrability.ComplexIntegrands
import SpherePacking.Dim8.MagicFunction.a.Integrability.RealIntegrands
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.BoundingAux
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.BoundingAuxIci
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I1
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I2
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I3
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I4
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I5
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.I6
import SpherePacking.Dim8.MagicFunction.a.IntegralEstimates.PowExpBounds
import SpherePacking.Dim8.MagicFunction.a.Schwartz.Basic
import SpherePacking.Dim8.MagicFunction.a.Schwartz.DecayI1
import SpherePacking.Dim8.MagicFunction.a.Schwartz.SmoothI1
import SpherePacking.Dim8.MagicFunction.a.Schwartz.SmoothI2
import SpherePacking.Dim8.MagicFunction.a.Schwartz.SmoothI4
import SpherePacking.Dim8.MagicFunction.a.Schwartz.SmoothI6
import SpherePacking.Dim8.MagicFunction.a.SpecialValues
import SpherePacking.Dim8.MagicFunction.b.Basic
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.FourierPermutations
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.GaussianFourier
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12ContourDeformation
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12CurveIntegrals
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12Defs
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12DiffContOnCl
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12FourierJ1
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12FourierJ1Kernel
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12FourierJ2
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ12Regularity
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ5
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.PermJ5Integrability
import SpherePacking.Dim8.MagicFunction.b.Eigenfunction.Prelude
import SpherePacking.Dim8.MagicFunction.b.Psi
import SpherePacking.Dim8.MagicFunction.b.PsiBounds
import SpherePacking.Dim8.MagicFunction.b.PsiParamRelations
import SpherePacking.Dim8.MagicFunction.b.Schwartz.Basic
import SpherePacking.Dim8.MagicFunction.b.Schwartz.BoundsAux
import SpherePacking.Dim8.MagicFunction.b.Schwartz.PsiExpBounds.Basic
import SpherePacking.Dim8.MagicFunction.b.Schwartz.PsiExpBounds.PsiSDecay
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ1
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ2
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ24Common
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ3
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ4
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ5
import SpherePacking.Dim8.MagicFunction.b.Schwartz.SmoothJ6.Bounds
import SpherePacking.Dim8.MagicFunction.b.SpecialValues
import SpherePacking.Dim8.MagicFunction.g.Basic
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.APrimeExtension
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.ImagAxis
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.Integrability
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.LargeImagApprox
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Continuation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Core
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.IntegralLemmas
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Parametric
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.A.Representation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.AnotherIntegral
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.BPrimeExtension
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.Cancellation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.Continuation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.Parametric
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.PsiICancellation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.HExpansions
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.InvH2Sq
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.QExpansion
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.Common
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.AnotherIntegral.ContinuationCommon
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.Defs
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.DeltaBounds
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.ImagAxisReal
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IneqA
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IneqB
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IneqCommon
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IntegralA
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IntegralB
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IntegralPieces
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IntegralReductions
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.IntegralReps.ACDomain
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceA.Basic
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceA.FiniteDifference
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceA.LaplaceRepresentation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceA.StripBounds
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceA.TailDeformation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceB.Basic
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceB.ContourIdentities
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceB.LaplaceRepresentation
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.LaplaceLemmas
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.PureImaginary
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.RealValued
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.ScaledMagic
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.SignConditions
import SpherePacking.Dim8.MagicFunction.g.CohnElkies.TheoremG1
import SpherePacking.Dim8.MainTheorem
import SpherePacking.Dim8.ScaledMagic
import SpherePacking.Dim8.UpperBound
import SpherePacking.ForMathlib.AtImInfty
import SpherePacking.ForMathlib.BoundsOnIcc
import SpherePacking.ForMathlib.CauchyGoursat.OpenRectangular
import SpherePacking.ForMathlib.ComplexI
import SpherePacking.ForMathlib.ContDiffOnByDeriv
import SpherePacking.ForMathlib.Cusps
import SpherePacking.ForMathlib.DerivHelpers
import SpherePacking.ForMathlib.ENNReal
import SpherePacking.ForMathlib.Encard
import SpherePacking.ForMathlib.ExpBounds
import SpherePacking.ForMathlib.ExpNormSqDiv
import SpherePacking.ForMathlib.ExpPiIMulMulI
import SpherePacking.ForMathlib.Fourier
import SpherePacking.ForMathlib.FourierLinearEquiv
import SpherePacking.ForMathlib.FourierPhase
import SpherePacking.ForMathlib.FunctionsBoundedAtInfty
import SpherePacking.ForMathlib.GaussianFourierCommon
import SpherePacking.ForMathlib.GaussianRexpIntegrable
import SpherePacking.ForMathlib.GaussianRexpIntegral
import SpherePacking.ForMathlib.IntegrablePowMulExp
import SpherePacking.ForMathlib.IntegralProd
import SpherePacking.ForMathlib.IntervalIntegral
import SpherePacking.ForMathlib.InvPowSummability
import SpherePacking.ForMathlib.IteratedDeriv
import SpherePacking.ForMathlib.RadialSchwartz.Cutoff
import SpherePacking.ForMathlib.RadialSchwartz.Multidimensional
import SpherePacking.ForMathlib.RadialSchwartz.OneSided
import SpherePacking.ForMathlib.ScalarOneForm
import SpherePacking.ForMathlib.ScalarOneFormDiffContOnCl
import SpherePacking.ForMathlib.ScalarOneFormFDeriv
import SpherePacking.ForMathlib.SigmaBounds
import SpherePacking.ForMathlib.SigmaSummability
import SpherePacking.ForMathlib.SlashActions
import SpherePacking.ForMathlib.SpecificLimits
import SpherePacking.ForMathlib.Tprod
import SpherePacking.ForMathlib.UpperHalfPlane
import SpherePacking.ForMathlib.VolumeOfBalls
import SpherePacking.ForMathlib.ZLattice
import SpherePacking.Integration.DifferentiationUnderIntegral
import SpherePacking.Integration.EndpointIntegrability
import SpherePacking.Integration.FubiniIoc01
import SpherePacking.Integration.InvChangeOfVariables
import SpherePacking.Integration.J6Integrable
import SpherePacking.Integration.Measure
import SpherePacking.Integration.SmoothIntegralCommon
import SpherePacking.Integration.SmoothIntegralIciOne
import SpherePacking.Integration.UpperHalfPlaneComp
import SpherePacking.MagicFunction.IntegralParametrisations
import SpherePacking.MagicFunction.IntegralParametrisationsContinuity
import SpherePacking.MagicFunction.PolyFourierCoeffBound
import SpherePacking.MagicFunction.PsiTPrimeZ1
import SpherePacking.MagicFunction.PsiTPrimeZ1Integrability
import SpherePacking.ModularForms.BigO
import SpherePacking.ModularForms.CLogArgLemmas
import SpherePacking.ModularForms.CSqrt
import SpherePacking.ModularForms.Cauchylems
import SpherePacking.ModularForms.CuspFormIsoModforms
import SpherePacking.ModularForms.Delta.Basic
import SpherePacking.ModularForms.Delta.ImagAxis
import SpherePacking.ModularForms.Derivative
import SpherePacking.ModularForms.DimGenCongLevels.Aux
import SpherePacking.ModularForms.DimGenCongLevels.Basic
import SpherePacking.ModularForms.DimGenCongLevels.FiniteDimensional
import SpherePacking.ModularForms.DimGenCongLevels.NormReduction
import SpherePacking.ModularForms.DimGenCongLevels.NormTransfer
import SpherePacking.ModularForms.DimensionFormulas
import SpherePacking.ModularForms.E2.Basic
import SpherePacking.ModularForms.E2.Transform
import SpherePacking.ModularForms.Eisenstein
import SpherePacking.ModularForms.EisensteinBase
import SpherePacking.ModularForms.Eisensteinqexpansions
import SpherePacking.ModularForms.Equivs
import SpherePacking.ModularForms.Eta
import SpherePacking.ModularForms.FG.AsymptoticsTools
import SpherePacking.ModularForms.FG.Basic
import SpherePacking.ModularForms.FG.Inequalities
import SpherePacking.ModularForms.FG.L10OverAsymptotics
import SpherePacking.ModularForms.FG.Positivity
import SpherePacking.ModularForms.IsCuspForm
import SpherePacking.ModularForms.IteratedDerivs
import SpherePacking.ModularForms.JacobiTheta
import SpherePacking.ModularForms.LimUnderLemmas
import SpherePacking.ModularForms.LogDerivLemmas
import SpherePacking.ModularForms.Lv1Lv2Identities
import SpherePacking.ModularForms.MultipliableLemmas
import SpherePacking.ModularForms.PhiTransform
import SpherePacking.ModularForms.PhiTransformLemmas
import SpherePacking.ModularForms.QExpansion
import SpherePacking.ModularForms.QExpansionLemmas.LimitsAtInfinity
import SpherePacking.ModularForms.QExpansionLemmas.QExpansionAlgebra
import SpherePacking.ModularForms.ResToImagAxis
import SpherePacking.ModularForms.SlashActionAuxil
import SpherePacking.ModularForms.SummableLemmas.Basic
import SpherePacking.ModularForms.SummableLemmas.Cotangent
import SpherePacking.ModularForms.SummableLemmas.G2
import SpherePacking.ModularForms.SummableLemmas.IntPNat
import SpherePacking.ModularForms.SummableLemmas.QExpansion
import SpherePacking.ModularForms.TSumDerivWithin
import SpherePacking.ModularForms.TendsToLemmas
import SpherePacking.ModularForms.ThetaDerivIdentities
import SpherePacking.Tactic.FunPropExt
import SpherePacking.Tactic.NormNumI
import SpherePacking.Tactic.Test.FunPropExt
import SpherePacking.Tactic.Test.NormNumI