Skip to content

Gauss: complete formalization of E₈ optimality in ℝ⁸ #341

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
augustepoiroux wants to merge 18 commits into
base: main
Choose a base branch
from
Draft

Gauss: complete formalization of E₈ optimality in ℝ⁸ #341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
d25e859
Full formalization
augustepoiroux Feb 23, 2026
38876bc
Add back corollary results + few bad merge conflict resolutions
augustepoiroux Feb 23, 2026
9d272f0
improvements found by tryAtEachStep
dwrensha Feb 23, 2026
92862ff
Merge pull request #1 from dwrensha/pr341-tryAtEachStep
augustepoiroux Feb 24, 2026
b6b9dff
Add back some corollary results + proofs golfed by Gauss that got wro…
augustepoiroux Feb 24, 2026
a1e0153
more improvements found by tryAtEachStep
dwrensha Feb 24, 2026
797bf3c
Merge pull request #2 from dwrensha/pr341-tryAtEachStep-2
augustepoiroux Feb 24, 2026
39ec25c
positivity improvements suggested by tryAtEachStep
dwrensha Feb 24, 2026
eae56f8
Merge pull request #4 from dwrensha/tryAtEachStep-positivity
augustepoiroux Feb 24, 2026
b59b31f
more golfs found by tryAtEachStep
dwrensha Feb 25, 2026
8c1ab42
Merge pull request #5 from dwrensha/tryAtEachStep-more
augustepoiroux Feb 25, 2026
5cbf8c4
Add improvements found by autoGolf + a few other golfs
augustepoiroux Feb 26, 2026
052fccb
Merge pull request #6 from math-inc/autoGolf-1
augustepoiroux Feb 26, 2026
e42c4a5
autoGolf + Gauss pass
augustepoiroux Mar 1, 2026
190c43b
More golfing
augustepoiroux Mar 1, 2026
958c514
Revert a few bad changes
augustepoiroux Mar 1, 2026
85af201
Few more golfs
augustepoiroux Mar 1, 2026
a604233
Merge pull request #7 from math-inc/autoGolf-2
augustepoiroux Mar 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
197 changes: 188 additions & 9 deletions SpherePacking.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,72 +1,248 @@
import SpherePacking.Basic.E8
import SpherePacking.Basic.PeriodicPacking
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.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.E8.Basic
import SpherePacking.E8.Packing
import SpherePacking.ForMathlib.Asymptotics
import SpherePacking.ForMathlib.AtImInfty
import SpherePacking.ForMathlib.BoundsOnIcc
import SpherePacking.ForMathlib.Cardinal
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.ENat
import SpherePacking.ForMathlib.Encard
import SpherePacking.ForMathlib.ExpBounds
import SpherePacking.ForMathlib.ExpNormSqDiv
import SpherePacking.ForMathlib.ExpPiIMulMulI
import SpherePacking.ForMathlib.Finsupp
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.InnerProductSpace
import SpherePacking.ForMathlib.IntegrablePowMulExp
import SpherePacking.ForMathlib.IntegralProd
import SpherePacking.ForMathlib.IntervalIntegral
import SpherePacking.ForMathlib.InvPowSummability
import SpherePacking.ForMathlib.IteratedDeriv
import SpherePacking.ForMathlib.MDifferentiableFunProp
import SpherePacking.ForMathlib.RadialSchwartz.Cutoff
import SpherePacking.ForMathlib.RadialSchwartz.Multidimensional
import SpherePacking.ForMathlib.RadialSchwartz.OneSided
import SpherePacking.ForMathlib.Real
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.UpperHalfPlane
import SpherePacking.ForMathlib.Vec
import SpherePacking.ForMathlib.VolumeOfBalls
import SpherePacking.ForMathlib.ZLattice
import SpherePacking.ForMathlib.tprod
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.MagicFunction.a.Basic
import SpherePacking.MagicFunction.a.Eigenfunction
import SpherePacking.MagicFunction.a.Eigenfunction.FourierPermutations
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12ContourAux
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12ContourMain
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12Fourier
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12FourierAux
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12FourierIntegrableI1
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12FourierIntegrableI2
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12FourierMain
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12Prelude
import SpherePacking.MagicFunction.a.Eigenfunction.PermI12WedgeDomain
import SpherePacking.MagicFunction.a.Eigenfunction.PermI5Integrability
import SpherePacking.MagicFunction.a.Eigenfunction.PermI5Kernel
import SpherePacking.MagicFunction.a.Eigenfunction.PermI5Main
import SpherePacking.MagicFunction.a.Integrability.ComplexIntegrands
import SpherePacking.MagicFunction.a.Integrability.Integrability
import SpherePacking.MagicFunction.a.Integrability.RealIntegrands
import SpherePacking.MagicFunction.a.IntegralEstimates.BoundingAux
import SpherePacking.MagicFunction.a.IntegralEstimates.BoundingAuxIci
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.IntegralEstimates.PowExpBounds
import SpherePacking.MagicFunction.a.Schwartz.Basic
import SpherePacking.MagicFunction.a.Schwartz.DecayI1
import SpherePacking.MagicFunction.a.Schwartz.SmoothI1
import SpherePacking.MagicFunction.a.Schwartz.SmoothI2
import SpherePacking.MagicFunction.a.Schwartz.SmoothI4
import SpherePacking.MagicFunction.a.Schwartz.SmoothI6
import SpherePacking.MagicFunction.a.SpecialValues
import SpherePacking.MagicFunction.b.Basic
import SpherePacking.MagicFunction.b.Eigenfunction
import SpherePacking.MagicFunction.b.Schwartz
import SpherePacking.MagicFunction.b.Eigenfunction.FourierPermutations
import SpherePacking.MagicFunction.b.Eigenfunction.GaussianFourier
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12ContourDeformation
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12CurveIntegrals
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12Defs
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12DiffContOnCl
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12FourierJ1
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12FourierJ1Kernel
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12FourierJ2
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ12Regularity
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ5
import SpherePacking.MagicFunction.b.Eigenfunction.PermJ5Integrability
import SpherePacking.MagicFunction.b.Eigenfunction.Prelude
import SpherePacking.MagicFunction.b.PsiBounds
import SpherePacking.MagicFunction.b.PsiParamRelations
import SpherePacking.MagicFunction.b.Schwartz.Basic
import SpherePacking.MagicFunction.b.Schwartz.BoundsAux
import SpherePacking.MagicFunction.b.Schwartz.PsiExpBounds.Basic
import SpherePacking.MagicFunction.b.Schwartz.PsiExpBounds.PsiSDecay
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ1
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ2
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ24Common
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ3
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ4
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ5
import SpherePacking.MagicFunction.b.Schwartz.SmoothJ6.Bounds
import SpherePacking.MagicFunction.b.SpecialValues
import SpherePacking.MagicFunction.b.psi
import SpherePacking.MagicFunction.g.Basic
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.APrimeExtension
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.ImagAxis
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.Integrability
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Cancellation.LargeImagApprox
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Continuation
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Core
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.IntegralLemmas
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Parametric
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.A.Representation
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.AnotherIntegral
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.BPrimeExtension
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.Cancellation
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.Continuation
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.Parametric
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.PsiICancellation
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.HExpansions
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.InvH2Sq
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.B.ThetaAxis.QExpansion
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.Common
import SpherePacking.MagicFunction.g.CohnElkies.AnotherIntegral.ContinuationCommon
import SpherePacking.MagicFunction.g.CohnElkies.Defs
import SpherePacking.MagicFunction.g.CohnElkies.DeltaBounds
import SpherePacking.MagicFunction.g.CohnElkies.ImagAxisReal
import SpherePacking.MagicFunction.g.CohnElkies.IneqA
import SpherePacking.MagicFunction.g.CohnElkies.IneqB
import SpherePacking.MagicFunction.g.CohnElkies.IneqCommon
import SpherePacking.MagicFunction.g.CohnElkies.IntegralA
import SpherePacking.MagicFunction.g.CohnElkies.IntegralB
import SpherePacking.MagicFunction.g.CohnElkies.IntegralPieces
import SpherePacking.MagicFunction.g.CohnElkies.IntegralReductions
import SpherePacking.MagicFunction.g.CohnElkies.IntegralReps.ACDomain
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceA.Basic
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceA.FiniteDifference
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceA.LaplaceRepresentation
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceA.StripBounds
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceA.TailDeformation
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceB.Basic
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceB.ContourIdentities
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceB.LaplaceRepresentation
import SpherePacking.MagicFunction.g.CohnElkies.LaplaceLemmas
import SpherePacking.MagicFunction.g.CohnElkies.PureImaginary
import SpherePacking.MagicFunction.g.CohnElkies.RealValued
import SpherePacking.MagicFunction.g.CohnElkies.ScaledMagic
import SpherePacking.MagicFunction.g.CohnElkies.SignConditions
import SpherePacking.MagicFunction.g.CohnElkies.TheoremG1
import SpherePacking.MainTheorem
import SpherePacking.ModularForms.BigO
import SpherePacking.ModularForms.Cauchylems
import SpherePacking.ModularForms.CuspFormIsoModforms
import SpherePacking.ModularForms.Delta
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
import SpherePacking.ModularForms.Eisenstein
import SpherePacking.ModularForms.EisensteinAsymptotics
import SpherePacking.ModularForms.EisensteinBase
import SpherePacking.ModularForms.Eisensteinqexpansions
import SpherePacking.ModularForms.FG
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.Icc_Ico_lems
import SpherePacking.ModularForms.IsCuspForm
import SpherePacking.ModularForms.JacobiTheta
import SpherePacking.ModularForms.Lv1Lv2Identities
import SpherePacking.ModularForms.PhiTransform
import SpherePacking.ModularForms.PhiTransformLemmas
import SpherePacking.ModularForms.QExpansion
import SpherePacking.ModularForms.RamanujanIdentities
import SpherePacking.ModularForms.ResToImagAxis
import SpherePacking.ModularForms.SerreDerivativeSlash
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.ThetaDerivIdentities
import SpherePacking.ModularForms.clog_arg_lems
import SpherePacking.ModularForms.csqrt
Expand All @@ -79,11 +255,14 @@ 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.ScaledMagic
import SpherePacking.Tactic.FunPropExt
import SpherePacking.Tactic.NormNumI
import SpherePacking.Tactic.NormNumI_Scratch
import SpherePacking.Tactic.Test.FunPropExt
import SpherePacking.Tactic.Test.NormNumI
import SpherePacking.UpperBound
22 changes: 22 additions & 0 deletions SpherePacking/Basic/Domains/RightHalfPlane.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module
public import Mathlib.Analysis.Complex.Basic

/-!
# The open right half-plane

This file defines `rightHalfPlane : Set ℂ`, the open right half-plane `{u : ℂ | 0 < u.re}`,
and records basic topological facts.
-/

namespace SpherePacking

/-! ## Definitions -/

/-- The open right half-plane `{u : ℂ | 0 < u.re}`. -/
@[expose] public def rightHalfPlane : Set ℂ := {u : ℂ | 0 < u.re}

/-- The right half-plane is an open subset of `ℂ`. -/
public lemma rightHalfPlane_isOpen : IsOpen rightHalfPlane := by
simpa [rightHalfPlane] using (isOpen_Ioi.preimage Complex.continuous_re)

end SpherePacking
Loading