Blueprint Summary🔗

Overview

Total entries111completed: 0; deps incomplete: 0; sorries: 74; no proof: 32

Ready now74Entries whose next formalization step is currently unblocked.

Fully closed0Local code and prerequisite closure are both complete.

Actionable priorities43Entries ready now and already unlocking downstream work.

Current blockers98Missing external or incomplete Lean declarations.

Ready next (43)

«lemma:psi-bound»(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 3downstream unlocks: 6proof: ready to formalize
«thm:serre-der-modularity»(Theorem)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 5proof: Lean code incomplete
Associated lean decls (1)
- serre_D_slash_invariant
«cor:disc-pos»(Corollary)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: Lean code incomplete
Associated lean decls (1)
- Delta_imag_axis_pos
«cor:theta-pos»(Corollary)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: Lean code incomplete
Associated lean decls (2)
- H₂_imag_axis_pos
- H₄_imag_axis_pos
«lemma:mod-div-disc-bound»(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: Lean code incomplete
Associated lean decls (1)
- MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
«thm:ramanujan-formula»(Theorem)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: Lean code incomplete
Associated lean decls (6)
«thm:serre-der-prod-rule»(Theorem)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 4proof: Lean code incomplete
Associated lean decls (1)
- serre_D_mul
«cor:phi0-bound»(Corollary)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 3proof: not ready
«thm:periodic-packing-optimal»(Theorem)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 3proof: Lean code incomplete
Associated lean decls (1)
- periodic_constant_eq_constant
«lemma:FG-de»(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 3proof: Lean code incomplete
Associated lean decls (2)
- MLDE_F
- MLDE_G
Show all 33 more priorities
- «cor:psiI-near-0-infty»(Corollary)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3proof: not ready
- «thm:anti-serre-der-pos»(Theorem)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3proof: not ready
- «lem:integral-bound»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 2proof: ready to formalize
- «thm:smooth-fast-decay-schwartz»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 2proof: ready to formalize
- «SpherePacking.scale_finiteDensity»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «lemma:Qlim»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lemma:log-der-inf»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
- «lemma:volume-ball-ratio-limit»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «prop:a-double-zeros»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
- «prop:a-fourier»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «prop:a0»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-fourier»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «prop:b0»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - MagicFunction.b.SpecialValues.b_zero
- «prop:ineqA»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
- «prop:ineqB»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
- «theorem:CE_Main»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: ready to formalize
- «thm:Poisson-summation-formula»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: Lean code incomplete
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- «cor:MLDE-pos»(Corollary)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: not ready
- «prop:b-double-zeros»(Lemma)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2proof: not ready
- «E8-defs-equivalent»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - span_E8Matrix
- «E8Packing-covol»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - E8Basis_volume
- «SpherePacking.scale_density»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - SpherePacking.scale_density
- «lemma:F-G-phi-psi-identities»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
- «lemma:F-G-pos»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «lemma:inv-power-summable»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
- «lemma:psi-new»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
- «prop:Qdec»(Lemma)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - FmodG_strictAntiOn
- «theorem:psp-density»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Ready for proof work.
  
  stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: Lean code incomplete
  Associated lean decls (1)
  - LinearProgrammingBound'
- «cor:phi2-bound»(Corollary)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: not ready
- «cor:phi4-bound»(Corollary)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: not ready
- «corollary:upper-bound-E8»(Corollary)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: not ready
- «thm:g1»(Theorem)
  
  Ready for statement work.
  
  stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: not ready

Current blockers (98)

«lemma:Ek-Fourier»(Lemma)

Axiom-like declaration: E_k_q_expansion [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:b0»(Lemma)

Axiom-like declaration: MagicFunction.b.SpecialValues.b_zero [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:a-definition»(Definition)

Axiom-like declaration: MagicFunction.a.RealIntegrals.a' [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:a-definition»(Definition)

Axiom-like declaration: MagicFunction.a.RadialFunctions.a [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-modular»(Lemma)

Axiom-like declaration: H₂_MF [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-modular»(Lemma)

Axiom-like declaration: H₃_MF [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-modular»(Lemma)

Axiom-like declaration: H₄_MF [definition; axiom-like; axiom-like (no body); refs: n/a]
MainTheorem(Corollary)

Axiom-like declaration: SpherePacking.MainTheorem [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₂_T_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₃_T_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₄_T_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₂_S_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₃_S_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:theta-transform-S-T»(Lemma)

Axiom-like declaration: H₄_S_action [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:Fourier-Transform»(Definition)

Axiom-like declaration: Real.fourierIntegral [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:dedekind_eta»(Definition)

Axiom-like declaration: η [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:periodic-packing-optimal»(Theorem)

Axiom-like declaration: periodic_constant_eq_constant [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.scale»(Definition)

Axiom-like declaration: SpherePacking.scale [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:serre-der-modularity»(Theorem)

Axiom-like declaration: serre_D_slash_invariant [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:Periodic-sphere-packing-constant»(Definition)

Axiom-like declaration: PeriodicSpherePackingConstant [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:Qlim»(Lemma)

Axiom-like declaration: FmodG_rightLimitAt_zero [definition; axiom-like; axiom-like (no body); refs: n/a]
E8Packing(Definition)

Axiom-like declaration: E8Packing [definition; axiom-like; axiom-like (no body); refs: n/a]
instLatticeE8(Lemma)

Axiom-like declaration: instIsZLatticeE8Lattice [definition; axiom-like; axiom-like (no body); refs: n/a]
PeriodicSpherePacking(Definition)

Axiom-like declaration: PeriodicSpherePacking [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:ineqAnew»(Corollary)

Axiom-like declaration: FG_inequality_1 [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:b-schwartz»(Lemma)

Axiom-like declaration: MagicFunction.FourierEigenfunctions.b [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-Matrix»(Definition)

Axiom-like declaration: E8Matrix [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-Set»(Definition)

Axiom-like declaration: Submodule.E8 [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:Poisson-summation-formula»(Theorem)

Axiom-like declaration: SchwartzMap.PoissonSummation_Lattices [definition; axiom-like; axiom-like (no body); refs: n/a]
SpherePackingConstant(Definition)

Axiom-like declaration: SpherePackingConstant [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:Fourier-transform-is-automorphism»(Lemma)

Axiom-like declaration: SchwartzMap.fourierTransformCLM [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:disc-definition»(Definition)

Axiom-like declaration: Δ [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.density»(Definition)

Axiom-like declaration: SpherePacking.density [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:dual-lattice»(Definition)

Axiom-like declaration: LinearMap.BilinForm.dualSubmodule [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-Lattice»(Lemma)

Axiom-like declaration: E8Lattice [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.constant_eq_constant_normalized»(Lemma)

Axiom-like declaration: SpherePacking.constant_eq_constant_normalized [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:jacobi-identity»(Lemma)

Axiom-like declaration: jacobi_identity [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:FG-de»(Lemma)

Axiom-like declaration: MLDE_F [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:FG-de»(Lemma)

Axiom-like declaration: MLDE_G [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:F-G-pos»(Lemma)

Axiom-like declaration: F_imag_axis_pos [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:F-G-pos»(Lemma)

Axiom-like declaration: G_imag_axis_pos [definition; axiom-like; axiom-like (no body); refs: n/a]
instDiscreteE8Lattice(Lemma)

Axiom-like declaration: instDiscreteE8Lattice [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:Ek»(Definition)

Axiom-like declaration: ModularForm.eisensteinSeries_MF [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:Schwartz-Space»(Definition)

Axiom-like declaration: SchwartzMap [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:Cohn-Elkies-general»(Theorem)

Axiom-like declaration: LinearProgrammingBound [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-is-basis»(Lemma)

Axiom-like declaration: span_E8Matrix_eq_top [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:volume-ball-ratio-limit»(Lemma)

Axiom-like declaration: volume_ball_ratio_tendsto_nhds_one'' [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:lattice-points-bound»(Lemma)

Axiom-like declaration: PeriodicSpherePacking.aux2_ge' [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:lattice-points-bound»(Lemma)

Axiom-like declaration: PeriodicSpherePacking.aux2_le' [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:sp-finite-density-bound»(Lemma)

Axiom-like declaration: SpherePacking.finiteDensity_le [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:sp-finite-density-bound»(Lemma)

Axiom-like declaration: SpherePacking.finiteDensity_ge [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:b-fourier»(Lemma)

Axiom-like declaration: MagicFunction.b.Fourier.eig_b [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₂ [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₄ [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₆ [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₂' [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₄' [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:ramanujan-formula»(Theorem)

Axiom-like declaration: ramanujan_E₆' [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.scale_density»(Lemma)

Axiom-like declaration: SpherePacking.scale_density [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:a0»(Lemma)

Axiom-like declaration: MagicFunction.a.SpecialValues.a_zero [definition; axiom-like; axiom-like (no body); refs: n/a]
«theorem:psp-density»(Theorem)

Axiom-like declaration: PeriodicSpherePacking.density_eq [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:Cohn-Elkies-periodic»(Theorem)

Axiom-like declaration: LinearProgrammingBound' [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:disc-nonvanishing»(Corollary)

Axiom-like declaration: Δ_ne_zero [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8Packing-density»(Theorem)

Axiom-like declaration: E8Packing_density [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:FG-definition»(Definition)

Axiom-like declaration: F [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:FG-definition»(Definition)

Axiom-like declaration: G [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:mod-div-disc-bound»(Lemma)

Axiom-like declaration: MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:ineqBnew»(Corollary)

Axiom-like declaration: FG_inequality_2 [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:a-fourier»(Lemma)

Axiom-like declaration: MagicFunction.a.Fourier.eig_a [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:H2-H3-H4»(Definition)

Axiom-like declaration: H₂ [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:H2-H3-H4»(Definition)

Axiom-like declaration: H₃ [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:H2-H3-H4»(Definition)

Axiom-like declaration: H₄ [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-vector-norms»(Lemma)

Axiom-like declaration: E8_norm_eq_sqrt_even [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.scale_finiteDensity»(Lemma)

Axiom-like declaration: SpherePacking.scale_finiteDensity [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:periodic-points-bounds»(Lemma)

Axiom-like declaration: PeriodicSpherePacking.aux_ge [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:periodic-points-bounds»(Lemma)

Axiom-like declaration: PeriodicSpherePacking.aux_le [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:slash-negI-even-weight»(Lemma)

Axiom-like declaration: modular_slash_negI_of_even [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:E2»(Definition)

Axiom-like declaration: E₂_eq [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:theta-pos»(Corollary)

Axiom-like declaration: H₂_imag_axis_pos [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:theta-pos»(Corollary)

Axiom-like declaration: H₄_imag_axis_pos [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:disc-cuspform»(Lemma)

Axiom-like declaration: Delta [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:th00-th01-th10»(Definition)

Axiom-like declaration: Θ₂ [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:th00-th01-th10»(Definition)

Axiom-like declaration: Θ₃ [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:th00-th01-th10»(Definition)

Axiom-like declaration: Θ₄ [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8-defs-equivalent»(Theorem)

Axiom-like declaration: span_E8Matrix [definition; axiom-like; axiom-like (no body); refs: n/a]
«E8Packing-covol»(Lemma)

Axiom-like declaration: E8Basis_volume [definition; axiom-like; axiom-like (no body); refs: n/a]
«thm:serre-der-prod-rule»(Theorem)

Axiom-like declaration: serre_D_mul [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.finiteDensity»(Definition)

Axiom-like declaration: SpherePacking.finiteDensity [definition; axiom-like; axiom-like (no body); refs: n/a]
IsZLattice(Definition)

Axiom-like declaration: IsZLattice [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:Ek-is-modular-form»(Lemma)

Axiom-like declaration: EisensteinSeries.eisensteinSeries_SIF [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:Mk»(Definition)

Axiom-like declaration: ModularForm [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:derivative»(Definition)

Axiom-like declaration: D [definition; axiom-like; axiom-like (no body); refs: n/a]
«SpherePacking.balls»(Definition)

Axiom-like declaration: SpherePacking.balls [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:Qdec»(Lemma)

Axiom-like declaration: FmodG_strictAntiOn [definition; axiom-like; axiom-like (no body); refs: n/a]
«cor:disc-pos»(Corollary)

Axiom-like declaration: Delta_imag_axis_pos [definition; axiom-like; axiom-like (no body); refs: n/a]
«prop:a-schwartz»(Lemma)

Axiom-like declaration: MagicFunction.FourierEigenfunctions.a [definition; axiom-like; axiom-like (no body); refs: n/a]
«lemma:E2-transform-S»(Lemma)

Axiom-like declaration: E₂_transform [definition; axiom-like; axiom-like (no body); refs: n/a]
«def:serre-der»(Definition)

Axiom-like declaration: serre_D [definition; axiom-like; axiom-like (no body); refs: n/a]

Entry index (111)

Definitions30completed: 0; deps incomplete: 0; sorries: 25; no proof: 0

Lemmas53completed: 0; deps incomplete: 0; sorries: 33; no proof: 20

Theorems15completed: 0; deps incomplete: 0; sorries: 10; no proof: 5

Corollaries13completed: 0; deps incomplete: 0; sorries: 6; no proof: 7

Axiom-like entries74completed: 0; deps incomplete: 0; sorries: 74; no proof: 0

Informal-only entries37

Definition Index (30)

«def:a-definition»(Definition)
Associated lean decls (2)
- MagicFunction.a.RealIntegrals.a'
- MagicFunction.a.RadialFunctions.a
«def:Fourier-Transform»(Definition)
Associated lean decls (1)
- Real.fourierIntegral
«def:dedekind_eta»(Definition)
Associated lean decls (1)
- η
«SpherePacking.scale»(Definition)
Associated lean decls (1)
- SpherePacking.scale
«def:Periodic-sphere-packing-constant»(Definition)
Associated lean decls (1)
- PeriodicSpherePackingConstant
E8Packing(Definition)
Associated lean decls (1)
- E8Packing
PeriodicSpherePacking(Definition)
Associated lean decls (1)
- PeriodicSpherePacking
«E8-Matrix»(Definition)
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)
Associated lean decls (1)
- Submodule.E8
SpherePackingConstant(Definition)
Associated lean decls (1)
- SpherePackingConstant
«def:disc-definition»(Definition)
Associated lean decls (1)
- Δ
«SpherePacking.density»(Definition)
Associated lean decls (1)
- SpherePacking.density
«def:dual-lattice»(Definition)
Associated lean decls (1)
- LinearMap.BilinForm.dualSubmodule
«def:h»(Definition)
«def:slash-operator»(Definition)
«def:Ek»(Definition)
Associated lean decls (1)
- ModularForm.eisensteinSeries_MF
«def:Schwartz-Space»(Definition)
Associated lean decls (1)
- SchwartzMap
«def:phi4-phi2-phi0»(Definition)
«def:psiI-psiT-psiS»(Definition)
«def:FG-definition»(Definition)
Associated lean decls (2)
- F
- G
«def:H2-H3-H4»(Definition)
Associated lean decls (3)
- H₂
- H₃
- H₄
«def:E2»(Definition)
Associated lean decls (1)
- E₂_eq
«def:b-definition»(Definition)
«def:th00-th01-th10»(Definition)
Associated lean decls (3)
- Θ₂
- Θ₃
- Θ₄
«SpherePacking.finiteDensity»(Definition)
Associated lean decls (1)
- SpherePacking.finiteDensity
IsZLattice(Definition)
Associated lean decls (1)
- IsZLattice
«def:Mk»(Definition)
Associated lean decls (1)
- ModularForm
«def:derivative»(Definition)
Associated lean decls (1)
- D
«SpherePacking.balls»(Definition)
Associated lean decls (1)
- SpherePacking.balls
«def:serre-der»(Definition)
Associated lean decls (1)
- serre_D

Theorem / Lemma / Corollary Index (81)

«lemma:Ek-Fourier»(Lemma)
Associated lean decls (1)
- E_k_q_expansion
«prop:b0»(Lemma)
Associated lean decls (1)
- MagicFunction.b.SpecialValues.b_zero
«lemma:psiI-psiT-psiS-fourier»(Lemma)
«lemma:theta-modular»(Lemma)
Associated lean decls (3)
MainTheorem(Corollary)
Associated lean decls (1)
- SpherePacking.MainTheorem
«lemma:theta-transform-S-T»(Lemma)
Associated lean decls (6)
«prop:a-double-zeros»(Lemma)
«thm:periodic-packing-optimal»(Theorem)
Associated lean decls (1)
- periodic_constant_eq_constant
«thm:serre-der-modularity»(Theorem)
Associated lean decls (1)
- serre_D_slash_invariant
«prop:ineqB»(Lemma)
«lemma:Qlim»(Lemma)
Associated lean decls (1)
- FmodG_rightLimitAt_zero
«lem:integral-bound»(Lemma)
«cor:phi0-bound»(Corollary)
«prop:ineqA»(Lemma)
instLatticeE8(Lemma)
Associated lean decls (1)
- instIsZLatticeE8Lattice
«thm:anti-serre-der-pos»(Theorem)
«cor:ineqAnew»(Corollary)
Associated lean decls (1)
- FG_inequality_1
«prop:b-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.b
«cor:phi0-near-0-infty»(Corollary)
«thm:Poisson-summation-formula»(Theorem)
Associated lean decls (1)
- SchwartzMap.PoissonSummation_Lattices
«lemma:lv1-lv2-identities»(Lemma)
«lemma:Fourier-transform-is-automorphism»(Lemma)
Associated lean decls (1)
- SchwartzMap.fourierTransformCLM
«cor:MLDE-pos»(Corollary)
«lemma:bound-J1-J3-J5»(Lemma)
«E8-Lattice»(Lemma)
Associated lean decls (1)
- E8Lattice
«lemma:ineqABnew-equiv»(Lemma)
«SpherePacking.constant_eq_constant_normalized»(Lemma)
Associated lean decls (1)
- SpherePacking.constant_eq_constant_normalized
«lemma:jacobi-identity»(Lemma)
Associated lean decls (1)
- jacobi_identity
«lemma:FG-de»(Lemma)
Associated lean decls (2)
- MLDE_F
- MLDE_G
«lemma:F-G-pos»(Lemma)
Associated lean decls (2)
- F_imag_axis_pos
- G_imag_axis_pos
«corollary:upper-bound-E8»(Corollary)
instDiscreteE8Lattice(Lemma)
Associated lean decls (1)
- instDiscreteE8Lattice
«lemma:psi-new»(Lemma)
«lemma:phi0-transform»(Lemma)
«thm:Cohn-Elkies-general»(Theorem)
Associated lean decls (1)
- LinearProgrammingBound
«E8-is-basis»(Lemma)
Associated lean decls (1)
- span_E8Matrix_eq_top
«prop:b-double-zeros»(Lemma)
«lemma:volume-ball-ratio-limit»(Lemma)
Associated lean decls (1)
- volume_ball_ratio_tendsto_nhds_one''
«lemma:lattice-points-bound»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux2_ge'
- PeriodicSpherePacking.aux2_le'
«lemma:sp-finite-density-bound»(Lemma)
Associated lean decls (2)
- SpherePacking.finiteDensity_le
- SpherePacking.finiteDensity_ge
«cor:phi2-bound»(Corollary)
«prop:b-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.b.Fourier.eig_b
«thm:ramanujan-formula»(Theorem)
Associated lean decls (6)
«SpherePacking.scale_density»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_density
«prop:a0»(Lemma)
Associated lean decls (1)
- MagicFunction.a.SpecialValues.a_zero
«lem:bound-I1-I3-I5»(Lemma)
«theorem:psp-density»(Theorem)
Associated lean decls (1)
- PeriodicSpherePacking.density_eq
«thm:Cohn-Elkies-periodic»(Theorem)
Associated lean decls (1)
- LinearProgrammingBound'
«cor:disc-nonvanishing»(Corollary)
Associated lean decls (1)
- Δ_ne_zero
«E8Packing-density»(Theorem)
Associated lean decls (1)
- E8Packing_density
«lemma:mod-div-disc-bound»(Lemma)
Associated lean decls (1)
- MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
«thm:g1»(Theorem)
«lemma:psi-bound»(Lemma)
«cor:psiI-near-0-infty»(Corollary)
«thm:g»(Theorem)
«cor:ineqBnew»(Corollary)
Associated lean decls (1)
- FG_inequality_2
«prop:a-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.a.Fourier.eig_a
«lemma:Schwartz-summable»(Lemma)
«lemma:F-G-phi-psi-identities»(Lemma)
«E8-vector-norms»(Lemma)
Associated lean decls (1)
- E8_norm_eq_sqrt_even
«SpherePacking.scale_finiteDensity»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_finiteDensity
«lemma:periodic-points-bounds»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux_ge
- PeriodicSpherePacking.aux_le
«lemma:inv-power-summable»(Lemma)
«lemma:slash-negI-even-weight»(Lemma)
Associated lean decls (1)
- modular_slash_negI_of_even
«lemma:log-der-inf»(Lemma)
«cor:theta-pos»(Corollary)
Associated lean decls (2)
- H₂_imag_axis_pos
- H₄_imag_axis_pos
«lemma:disc-cuspform»(Lemma)
Associated lean decls (1)
- Delta
«E8-defs-equivalent»(Theorem)
Associated lean decls (1)
- span_E8Matrix
«E8Packing-covol»(Lemma)
Associated lean decls (1)
- E8Basis_volume
«thm:serre-der-prod-rule»(Theorem)
Associated lean decls (1)
- serre_D_mul
«lemma:Gaussian-Fourier»(Lemma)
«lemma:Ek-is-modular-form»(Lemma)
Associated lean decls (1)
- EisensteinSeries.eisensteinSeries_SIF
«prop:Qdec»(Lemma)
Associated lean decls (1)
- FmodG_strictAntiOn
«cor:disc-pos»(Corollary)
Associated lean decls (1)
- Delta_imag_axis_pos
«theorem:CE_Main»(Theorem)
«prop:a-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.a
«thm:smooth-fast-decay-schwartz»(Theorem)
«lemma:E2-transform-S»(Lemma)
Associated lean decls (1)
- E₂_transform
«lemma:bound-J2-J4-J6»(Lemma)
«lem:bound-I2-I4-I6»(Lemma)
«cor:phi4-bound»(Corollary)

By parent groups (19)

Periodic and lattice packings as a reduced optimization class. (1)

«thm:periodic-packing-optimal»(Theorem)
Associated lean decls (1)
- periodic_constant_eq_constant

Auxiliary functions <missing> and reformulation of inequalities. (6)

«lemma:F-G-phi-psi-identities»(Lemma)
«lemma:F-G-pos»(Lemma)
Associated lean decls (2)
- F_imag_axis_pos
- G_imag_axis_pos
«lemma:ineqABnew-equiv»(Lemma)
«cor:ineqAnew»(Corollary)
Associated lean decls (1)
- FG_inequality_1
«prop:ineqA»(Lemma)
«prop:ineqB»(Lemma)

Summability lemmas and Poisson summation over lattices. (4)

«thm:smooth-fast-decay-schwartz»(Theorem)
«lemma:inv-power-summable»(Lemma)
«lemma:Schwartz-summable»(Lemma)
«thm:Poisson-summation-formula»(Theorem)
Associated lean decls (1)
- SchwartzMap.PoissonSummation_Lattices

Auxiliary modular expressions and integral formulas defining <missing> . (5)

«cor:phi4-bound»(Corollary)
«lemma:mod-div-disc-bound»(Lemma)
Associated lean decls (1)
- MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
«cor:phi2-bound»(Corollary)
«lemma:phi0-transform»(Lemma)
«cor:phi0-bound»(Corollary)

Auxiliary forms and integral formulas defining <missing> . (2)

«lemma:psi-new»(Lemma)
«lemma:psiI-psiT-psiS-fourier»(Lemma)

Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (8)

«lemma:bound-J2-J4-J6»(Lemma)
«cor:psiI-near-0-infty»(Corollary)
«lemma:psi-bound»(Lemma)
«prop:b-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.b.Fourier.eig_b
«prop:b-double-zeros»(Lemma)
«lemma:bound-J1-J3-J5»(Lemma)
«prop:b-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.b
«prop:b0»(Lemma)
Associated lean decls (1)
- MagicFunction.b.SpecialValues.b_zero

Volume-count asymptotics for lattice and periodic center sets. (3)

«lemma:periodic-points-bounds»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux_ge
- PeriodicSpherePacking.aux_le
«lemma:lattice-points-bound»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux2_ge'
- PeriodicSpherePacking.aux2_le'
«lemma:volume-ball-ratio-limit»(Lemma)
Associated lean decls (1)
- volume_ball_ratio_tendsto_nhds_one''

Eisenstein series, the discriminant form, and positivity/nonvanishing tools. (6)

«lemma:E2-transform-S»(Lemma)
Associated lean decls (1)
- E₂_transform
«cor:disc-pos»(Corollary)
Associated lean decls (1)
- Delta_imag_axis_pos
«lemma:Ek-is-modular-form»(Lemma)
Associated lean decls (1)
- EisensteinSeries.eisensteinSeries_SIF
«lemma:disc-cuspform»(Lemma)
Associated lean decls (1)
- Delta
«cor:disc-nonvanishing»(Corollary)
Associated lean decls (1)
- Δ_ne_zero
«lemma:Ek-Fourier»(Lemma)
Associated lean decls (1)
- E_k_q_expansion

Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (8)

«lem:bound-I2-I4-I6»(Lemma)
«prop:a-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.a
«prop:a-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.a.Fourier.eig_a
«lem:bound-I1-I3-I5»(Lemma)
«prop:a0»(Lemma)
Associated lean decls (1)
- MagicFunction.a.SpecialValues.a_zero
«cor:phi0-near-0-infty»(Corollary)
«lem:integral-bound»(Lemma)
«prop:a-double-zeros»(Lemma)

Fourier transform and Schwartz-space preliminaries. (2)

«lemma:Gaussian-Fourier»(Lemma)
«lemma:Fourier-transform-is-automorphism»(Lemma)
Associated lean decls (1)
- SchwartzMap.fourierTransformCLM

Equivalent models of the <missing> lattice. (1)

«E8-defs-equivalent»(Theorem)
Associated lean decls (1)
- span_E8Matrix

Basic structural and arithmetic properties of <missing> . (5)

«E8-vector-norms»(Lemma)
Associated lean decls (1)
- E8_norm_eq_sqrt_even
«E8-is-basis»(Lemma)
Associated lean decls (1)
- span_E8Matrix_eq_top
instDiscreteE8Lattice(Lemma)
Associated lean decls (1)
- instDiscreteE8Lattice
«E8-Lattice»(Lemma)
Associated lean decls (1)
- E8Lattice
instLatticeE8(Lemma)
Associated lean decls (1)
- instIsZLatticeE8Lattice

Differential equations and monotonicity control. (6)

«prop:Qdec»(Lemma)
Associated lean decls (1)
- FmodG_strictAntiOn
«lemma:log-der-inf»(Lemma)
«cor:ineqBnew»(Corollary)
Associated lean decls (1)
- FG_inequality_2
«lemma:FG-de»(Lemma)
Associated lean decls (2)
- MLDE_F
- MLDE_G
«cor:MLDE-pos»(Corollary)
«lemma:Qlim»(Lemma)
Associated lean decls (1)
- FmodG_rightLimitAt_zero

Scaling invariance of finite density and asymptotic density. (3)

«SpherePacking.scale_finiteDensity»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_finiteDensity
«SpherePacking.scale_density»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_density
«SpherePacking.constant_eq_constant_normalized»(Lemma)
Associated lean decls (1)
- SpherePacking.constant_eq_constant_normalized

Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (3)

«theorem:CE_Main»(Theorem)
«corollary:upper-bound-E8»(Corollary)
MainTheorem(Corollary)
Associated lean decls (1)
- SpherePacking.MainTheorem

Congruence groups, slash operators, and modular forms. (1)

«lemma:slash-negI-even-weight»(Lemma)
Associated lean decls (1)
- modular_slash_negI_of_even

Serre derivative identities and differential inequalities. (4)

«thm:serre-der-prod-rule»(Theorem)
Associated lean decls (1)
- serre_D_mul
«thm:ramanujan-formula»(Theorem)
Associated lean decls (6)
«thm:anti-serre-der-pos»(Theorem)
«thm:serre-der-modularity»(Theorem)
Associated lean decls (1)
- serre_D_slash_invariant

Definition and density computation of the <missing> sphere packing. (2)

«E8Packing-covol»(Lemma)
Associated lean decls (1)
- E8Basis_volume
«E8Packing-density»(Theorem)
Associated lean decls (1)
- E8Packing_density

Theta constants and identities used in the magic-function construction. (5)

«cor:theta-pos»(Corollary)
Associated lean decls (2)
- H₂_imag_axis_pos
- H₄_imag_axis_pos
«lemma:jacobi-identity»(Lemma)
Associated lean decls (1)
- jacobi_identity
«lemma:lv1-lv2-identities»(Lemma)
«lemma:theta-transform-S-T»(Lemma)
Associated lean decls (6)
«lemma:theta-modular»(Lemma)
Associated lean decls (3)

Axiom-like Index (74)

«lemma:Ek-Fourier»(Lemma)
Associated lean decls (1)
- E_k_q_expansion
«prop:b0»(Lemma)
Associated lean decls (1)
- MagicFunction.b.SpecialValues.b_zero
«def:a-definition»(Definition)
Associated lean decls (2)
- MagicFunction.a.RealIntegrals.a'
- MagicFunction.a.RadialFunctions.a
«lemma:theta-modular»(Lemma)
Associated lean decls (3)
MainTheorem(Corollary)
Associated lean decls (1)
- SpherePacking.MainTheorem
«lemma:theta-transform-S-T»(Lemma)
Associated lean decls (6)
«def:Fourier-Transform»(Definition)
Associated lean decls (1)
- Real.fourierIntegral
«def:dedekind_eta»(Definition)
Associated lean decls (1)
- η
«thm:periodic-packing-optimal»(Theorem)
Associated lean decls (1)
- periodic_constant_eq_constant
«SpherePacking.scale»(Definition)
Associated lean decls (1)
- SpherePacking.scale
«thm:serre-der-modularity»(Theorem)
Associated lean decls (1)
- serre_D_slash_invariant
«def:Periodic-sphere-packing-constant»(Definition)
Associated lean decls (1)
- PeriodicSpherePackingConstant
«lemma:Qlim»(Lemma)
Associated lean decls (1)
- FmodG_rightLimitAt_zero
E8Packing(Definition)
Associated lean decls (1)
- E8Packing
instLatticeE8(Lemma)
Associated lean decls (1)
- instIsZLatticeE8Lattice
PeriodicSpherePacking(Definition)
Associated lean decls (1)
- PeriodicSpherePacking
«cor:ineqAnew»(Corollary)
Associated lean decls (1)
- FG_inequality_1
«prop:b-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.b
«E8-Matrix»(Definition)
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)
Associated lean decls (1)
- Submodule.E8
«thm:Poisson-summation-formula»(Theorem)
Associated lean decls (1)
- SchwartzMap.PoissonSummation_Lattices
SpherePackingConstant(Definition)
Associated lean decls (1)
- SpherePackingConstant
«lemma:Fourier-transform-is-automorphism»(Lemma)
Associated lean decls (1)
- SchwartzMap.fourierTransformCLM
«def:disc-definition»(Definition)
Associated lean decls (1)
- Δ
«SpherePacking.density»(Definition)
Associated lean decls (1)
- SpherePacking.density
«def:dual-lattice»(Definition)
Associated lean decls (1)
- LinearMap.BilinForm.dualSubmodule
«E8-Lattice»(Lemma)
Associated lean decls (1)
- E8Lattice
«SpherePacking.constant_eq_constant_normalized»(Lemma)
Associated lean decls (1)
- SpherePacking.constant_eq_constant_normalized
«lemma:jacobi-identity»(Lemma)
Associated lean decls (1)
- jacobi_identity
«lemma:FG-de»(Lemma)
Associated lean decls (2)
- MLDE_F
- MLDE_G
«lemma:F-G-pos»(Lemma)
Associated lean decls (2)
- F_imag_axis_pos
- G_imag_axis_pos
instDiscreteE8Lattice(Lemma)
Associated lean decls (1)
- instDiscreteE8Lattice
«def:Ek»(Definition)
Associated lean decls (1)
- ModularForm.eisensteinSeries_MF
«def:Schwartz-Space»(Definition)
Associated lean decls (1)
- SchwartzMap
«thm:Cohn-Elkies-general»(Theorem)
Associated lean decls (1)
- LinearProgrammingBound
«E8-is-basis»(Lemma)
Associated lean decls (1)
- span_E8Matrix_eq_top
«lemma:volume-ball-ratio-limit»(Lemma)
Associated lean decls (1)
- volume_ball_ratio_tendsto_nhds_one''
«lemma:lattice-points-bound»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux2_ge'
- PeriodicSpherePacking.aux2_le'
«lemma:sp-finite-density-bound»(Lemma)
Associated lean decls (2)
- SpherePacking.finiteDensity_le
- SpherePacking.finiteDensity_ge
«prop:b-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.b.Fourier.eig_b
«thm:ramanujan-formula»(Theorem)
Associated lean decls (6)
«SpherePacking.scale_density»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_density
«prop:a0»(Lemma)
Associated lean decls (1)
- MagicFunction.a.SpecialValues.a_zero
«theorem:psp-density»(Theorem)
Associated lean decls (1)
- PeriodicSpherePacking.density_eq
«thm:Cohn-Elkies-periodic»(Theorem)
Associated lean decls (1)
- LinearProgrammingBound'
«cor:disc-nonvanishing»(Corollary)
Associated lean decls (1)
- Δ_ne_zero
«E8Packing-density»(Theorem)
Associated lean decls (1)
- E8Packing_density
«def:FG-definition»(Definition)
Associated lean decls (2)
- F
- G
«lemma:mod-div-disc-bound»(Lemma)
Associated lean decls (1)
- MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
«cor:ineqBnew»(Corollary)
Associated lean decls (1)
- FG_inequality_2
«prop:a-fourier»(Lemma)
Associated lean decls (1)
- MagicFunction.a.Fourier.eig_a
«def:H2-H3-H4»(Definition)
Associated lean decls (3)
- H₂
- H₃
- H₄
«E8-vector-norms»(Lemma)
Associated lean decls (1)
- E8_norm_eq_sqrt_even
«SpherePacking.scale_finiteDensity»(Lemma)
Associated lean decls (1)
- SpherePacking.scale_finiteDensity
«lemma:periodic-points-bounds»(Lemma)
Associated lean decls (2)
- PeriodicSpherePacking.aux_ge
- PeriodicSpherePacking.aux_le
«lemma:slash-negI-even-weight»(Lemma)
Associated lean decls (1)
- modular_slash_negI_of_even
«def:E2»(Definition)
Associated lean decls (1)
- E₂_eq
«cor:theta-pos»(Corollary)
Associated lean decls (2)
- H₂_imag_axis_pos
- H₄_imag_axis_pos
«lemma:disc-cuspform»(Lemma)
Associated lean decls (1)
- Delta
«def:th00-th01-th10»(Definition)
Associated lean decls (3)
- Θ₂
- Θ₃
- Θ₄
«E8-defs-equivalent»(Theorem)
Associated lean decls (1)
- span_E8Matrix
«E8Packing-covol»(Lemma)
Associated lean decls (1)
- E8Basis_volume
«thm:serre-der-prod-rule»(Theorem)
Associated lean decls (1)
- serre_D_mul
«SpherePacking.finiteDensity»(Definition)
Associated lean decls (1)
- SpherePacking.finiteDensity
IsZLattice(Definition)
Associated lean decls (1)
- IsZLattice
«lemma:Ek-is-modular-form»(Lemma)
Associated lean decls (1)
- EisensteinSeries.eisensteinSeries_SIF
«def:Mk»(Definition)
Associated lean decls (1)
- ModularForm
«def:derivative»(Definition)
Associated lean decls (1)
- D
«SpherePacking.balls»(Definition)
Associated lean decls (1)
- SpherePacking.balls
«prop:Qdec»(Lemma)
Associated lean decls (1)
- FmodG_strictAntiOn
«cor:disc-pos»(Corollary)
Associated lean decls (1)
- Delta_imag_axis_pos
«prop:a-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.a
«lemma:E2-transform-S»(Lemma)
Associated lean decls (1)
- E₂_transform
«def:serre-der»(Definition)
Associated lean decls (1)
- serre_D

Dependency insights

Proof-used entries43Entries reused in proof-only dependencies.

Tracked parent groups20Grouped health rollups for parents with more than one child entry.

Most used in proofs (43)

«lemma:psi-bound»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 6
«cor:phi0-bound»(Corollary)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
«thm:periodic-packing-optimal»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- periodic_constant_eq_constant
«lem:integral-bound»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
«thm:smooth-fast-decay-schwartz»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
«thm:serre-der-modularity»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
- serre_D_slash_invariant
«cor:disc-pos»(Corollary)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- Delta_imag_axis_pos
«cor:theta-pos»(Corollary)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
- H₂_imag_axis_pos
- H₄_imag_axis_pos
«lemma:mod-div-disc-bound»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
«thm:ramanujan-formula»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (6)
Show all 33 more proof-used entries
- «thm:serre-der-prod-rule»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - serre_D_mul
- «cor:psiI-near-0-infty»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
- «lemma:FG-de»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - MLDE_F
  - MLDE_G
- «thm:anti-serre-der-pos»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
- «SpherePacking.scale_finiteDensity»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «cor:MLDE-pos»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «lemma:Qlim»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lemma:log-der-inf»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «lemma:volume-ball-ratio-limit»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «prop:a-double-zeros»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «prop:a-fourier»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «prop:a0»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-double-zeros»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «prop:b-fourier»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «prop:b0»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - MagicFunction.b.SpecialValues.b_zero
- «prop:ineqA»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «prop:ineqB»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «theorem:CE_Main»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
- «thm:Poisson-summation-formula»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- «E8-defs-equivalent»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - span_E8Matrix
- «E8Packing-covol»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - E8Basis_volume
- «SpherePacking.scale_density»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - SpherePacking.scale_density
- «cor:phi2-bound»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «cor:phi4-bound»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «corollary:upper-bound-E8»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «lemma:F-G-phi-psi-identities»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «lemma:F-G-pos»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «lemma:inv-power-summable»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «lemma:psi-new»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
- «prop:Qdec»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - FmodG_strictAntiOn
- «theorem:psp-density»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LinearProgrammingBound'
- «thm:g1»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1

Group health (20)

Eisenstein series, the discriminant form, and positivity/nonvanishing tools.eisenstein_discriminant

Grouped view over entries sharing the same parent.

total: 10closed: 0local-only: 0ready: 10blocked: 0incomplete Lean: 10unlock score: 4

Next: «cor:disc-pos» stage: proofdownstream unlocks: 4
Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .magic_b_properties

Grouped view over entries sharing the same parent.

total: 8closed: 0local-only: 0ready: 8blocked: 0incomplete Lean: 3unlock score: 15

Next: «lemma:psi-bound» stage: proofdownstream unlocks: 6
Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .magic_a_properties

Grouped view over entries sharing the same parent.

total: 8closed: 0local-only: 0ready: 8blocked: 0incomplete Lean: 3unlock score: 8

Next: «lem:integral-bound» stage: proofdownstream unlocks: 2
Auxiliary modular expressions and integral formulas defining <missing> .magic_phi_construction

Grouped view over entries sharing the same parent.

total: 7closed: 0local-only: 0ready: 7blocked: 0incomplete Lean: 2unlock score: 9

Next: «lemma:mod-div-disc-bound» stage: proofdownstream unlocks: 4
Auxiliary functions <missing> and reformulation of inequalities.fg_setup

Grouped view over entries sharing the same parent.

total: 7closed: 0local-only: 0ready: 7blocked: 0incomplete Lean: 3unlock score: 6

Next: «prop:ineqA» stage: proofdownstream unlocks: 2
Theta constants and identities used in the magic-function construction.theta_and_identities

Grouped view over entries sharing the same parent.

total: 7closed: 0local-only: 0ready: 7blocked: 0incomplete Lean: 6unlock score: 4

Next: «cor:theta-pos» stage: proofdownstream unlocks: 4
Serre derivative identities and differential inequalities.serre_derivative

Grouped view over entries sharing the same parent.

total: 6closed: 0local-only: 0ready: 6blocked: 0incomplete Lean: 5unlock score: 16

Next: «thm:serre-der-modularity» stage: proofdownstream unlocks: 5
Differential equations and monotonicity control.fg_differential

Grouped view over entries sharing the same parent.

total: 6closed: 0local-only: 0ready: 6blocked: 0incomplete Lean: 4unlock score: 10

Next: «lemma:FG-de» stage: proofdownstream unlocks: 3
Periodic and lattice packings as a reduced optimization class.periodic_packings

Grouped view over entries sharing the same parent.

total: 5closed: 0local-only: 0ready: 5blocked: 0incomplete Lean: 5unlock score: 3

Next: «thm:periodic-packing-optimal» stage: proofdownstream unlocks: 3
Auxiliary forms and integral formulas defining <missing> .magic_psi_construction

Grouped view over entries sharing the same parent.

total: 5closed: 0local-only: 0ready: 5blocked: 0incomplete Lean: 0unlock score: 1

Next: «lemma:psi-new» stage: proofdownstream unlocks: 1
Show all 10 more groups
- Basic structural and arithmetic properties of <missing> .e8_properties
  
  Grouped view over entries sharing the same parent.
  
  total: 5closed: 0local-only: 0ready: 5blocked: 0incomplete Lean: 5unlock score: 0
  
  Next: no ready child currently unlocks downstream work.
- Summability lemmas and Poisson summation over lattices.poisson_formula
  
  Grouped view over entries sharing the same parent.
  
  total: 4closed: 0local-only: 0ready: 4blocked: 0incomplete Lean: 1unlock score: 5
  
  Next: «thm:smooth-fast-decay-schwartz» stage: proofdownstream unlocks: 2
- Scaling invariance of finite density and asymptotic density.sphere_scaling
  
  Grouped view over entries sharing the same parent.
  
  total: 4closed: 0local-only: 0ready: 4blocked: 0incomplete Lean: 4unlock score: 3
  
  Next: «SpherePacking.scale_finiteDensity» stage: proofdownstream unlocks: 2
- Definitions of sphere packings, density, and the optimization target.sphere_setup
  
  Grouped view over entries sharing the same parent.
  
  total: 4closed: 0local-only: 0ready: 4blocked: 0incomplete Lean: 4unlock score: 0
  
  Next: no ready child currently unlocks downstream work.
- Fourier transform and Schwartz-space preliminaries.fourier_setup
  
  Grouped view over entries sharing the same parent.
  
  total: 4closed: 0local-only: 0ready: 4blocked: 0incomplete Lean: 3unlock score: 0
  
  Next: no ready child currently unlocks downstream work.
- Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.sphere_main_statement
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 1unlock score: 3
  
  Next: «theorem:CE_Main» stage: proofdownstream unlocks: 2
- Volume-count asymptotics for lattice and periodic center sets.density_periodic_counts
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 3unlock score: 2
  
  Next: «lemma:volume-ball-ratio-limit» stage: proofdownstream unlocks: 2
- Definition and density computation of the <missing> sphere packing.e8_density
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 3unlock score: 1
  
  Next: «E8Packing-covol» stage: proofdownstream unlocks: 1
- Equivalent models of the <missing> lattice.e8_definitions
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 3unlock score: 1
  
  Next: «E8-defs-equivalent» stage: proofdownstream unlocks: 1
- Congruence groups, slash operators, and modular forms.modular_forms_setup
  
  Grouped view over entries sharing the same parent.
  
  total: 3closed: 0local-only: 0ready: 3blocked: 0incomplete Lean: 2unlock score: 0
  
  Next: no ready child currently unlocks downstream work.

Metadata

Metadata audit

Missing owner111

Missing effort111

Untagged111

Missing owner (111)

E8Packing(Definition)

Missing owner metadata.
Associated lean decls (1)
- E8Packing
IsZLattice(Definition)

Missing owner metadata.
Associated lean decls (1)
- IsZLattice
MainTheorem(Corollary)

Missing owner metadata.
Associated lean decls (1)
- SpherePacking.MainTheorem
PeriodicSpherePacking(Definition)

Missing owner metadata.
Associated lean decls (1)
- PeriodicSpherePacking
SpherePackingConstant(Definition)

Missing owner metadata.
Associated lean decls (1)
- SpherePackingConstant
instDiscreteE8Lattice(Lemma)

Missing owner metadata.
Associated lean decls (1)
- instDiscreteE8Lattice
instLatticeE8(Lemma)

Missing owner metadata.
Associated lean decls (1)
- instIsZLatticeE8Lattice
«E8-Lattice»(Lemma)

Missing owner metadata.
Associated lean decls (1)
- E8Lattice
«E8-Matrix»(Definition)

Missing owner metadata.
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Submodule.E8
Show all 101 more entries missing owner
- «E8-defs-equivalent»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - span_E8Matrix
- «E8-is-basis»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - span_E8Matrix_eq_top
- «E8-vector-norms»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E8_norm_eq_sqrt_even
- «E8Packing-covol»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E8Basis_volume
- «E8Packing-density»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E8Packing_density
- «SpherePacking.balls»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.balls
- «SpherePacking.constant_eq_constant_normalized»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.constant_eq_constant_normalized
- «SpherePacking.density»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.density
- «SpherePacking.finiteDensity»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.finiteDensity
- «SpherePacking.scale_density»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.scale_density
- «SpherePacking.scale_finiteDensity»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «SpherePacking.scale»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SpherePacking.scale
- «cor:MLDE-pos»(Corollary)
  
  Missing owner metadata.
- «cor:disc-nonvanishing»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Δ_ne_zero
- «cor:disc-pos»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Delta_imag_axis_pos
- «cor:ineqAnew»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FG_inequality_1
- «cor:ineqBnew»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FG_inequality_2
- «cor:phi0-bound»(Corollary)
  
  Missing owner metadata.
- «cor:phi0-near-0-infty»(Corollary)
  
  Missing owner metadata.
- «cor:phi2-bound»(Corollary)
  
  Missing owner metadata.
- «cor:phi4-bound»(Corollary)
  
  Missing owner metadata.
- «cor:psiI-near-0-infty»(Corollary)
  
  Missing owner metadata.
- «cor:theta-pos»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - H₂_imag_axis_pos
  - H₄_imag_axis_pos
- «corollary:upper-bound-E8»(Corollary)
  
  Missing owner metadata.
- «def:E2»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E₂_eq
- «def:Ek»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ModularForm.eisensteinSeries_MF
- «def:FG-definition»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - F
  - G
- «def:Fourier-Transform»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Real.fourierIntegral
- «def:H2-H3-H4»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
  - H₂
  - H₃
  - H₄
- «def:Mk»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - ModularForm
- «def:Periodic-sphere-packing-constant»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - PeriodicSpherePackingConstant
- «def:Schwartz-Space»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SchwartzMap
- «def:a-definition»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MagicFunction.a.RealIntegrals.a'
  - MagicFunction.a.RadialFunctions.a
- «def:b-definition»(Definition)
  
  Missing owner metadata.
- «def:dedekind_eta»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - η
- «def:derivative»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - D
- «def:disc-definition»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Δ
- «def:dual-lattice»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LinearMap.BilinForm.dualSubmodule
- «def:h»(Definition)
  
  Missing owner metadata.
- «def:phi4-phi2-phi0»(Definition)
  
  Missing owner metadata.
- «def:psiI-psiT-psiS»(Definition)
  
  Missing owner metadata.
- «def:serre-der»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - serre_D
- «def:slash-operator»(Definition)
  
  Missing owner metadata.
- «def:th00-th01-th10»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
  - Θ₂
  - Θ₃
  - Θ₄
- «lem:bound-I1-I3-I5»(Lemma)
  
  Missing owner metadata.
- «lem:bound-I2-I4-I6»(Lemma)
  
  Missing owner metadata.
- «lem:integral-bound»(Lemma)
  
  Missing owner metadata.
- «lemma:E2-transform-S»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E₂_transform
- «lemma:Ek-Fourier»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - E_k_q_expansion
- «lemma:Ek-is-modular-form»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - EisensteinSeries.eisensteinSeries_SIF
- «lemma:F-G-phi-psi-identities»(Lemma)
  
  Missing owner metadata.
- «lemma:F-G-pos»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «lemma:FG-de»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MLDE_F
  - MLDE_G
- «lemma:Fourier-transform-is-automorphism»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SchwartzMap.fourierTransformCLM
- «lemma:Gaussian-Fourier»(Lemma)
  
  Missing owner metadata.
- «lemma:Qlim»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lemma:Schwartz-summable»(Lemma)
  
  Missing owner metadata.
- «lemma:bound-J1-J3-J5»(Lemma)
  
  Missing owner metadata.
- «lemma:bound-J2-J4-J6»(Lemma)
  
  Missing owner metadata.
- «lemma:disc-cuspform»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Delta
- «lemma:ineqABnew-equiv»(Lemma)
  
  Missing owner metadata.
- «lemma:inv-power-summable»(Lemma)
  
  Missing owner metadata.
- «lemma:jacobi-identity»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - jacobi_identity
- «lemma:lattice-points-bound»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux2_ge'
  - PeriodicSpherePacking.aux2_le'
- «lemma:log-der-inf»(Lemma)
  
  Missing owner metadata.
- «lemma:lv1-lv2-identities»(Lemma)
  
  Missing owner metadata.
- «lemma:mod-div-disc-bound»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
- «lemma:periodic-points-bounds»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux_ge
  - PeriodicSpherePacking.aux_le
- «lemma:phi0-transform»(Lemma)
  
  Missing owner metadata.
- «lemma:psi-bound»(Lemma)
  
  Missing owner metadata.
- «lemma:psi-new»(Lemma)
  
  Missing owner metadata.
- «lemma:psiI-psiT-psiS-fourier»(Lemma)
  
  Missing owner metadata.
- «lemma:slash-negI-even-weight»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - modular_slash_negI_of_even
- «lemma:sp-finite-density-bound»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - SpherePacking.finiteDensity_le
  - SpherePacking.finiteDensity_ge
- «lemma:theta-modular»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lemma:theta-transform-S-T»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lemma:volume-ball-ratio-limit»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «prop:Qdec»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FmodG_strictAntiOn
- «prop:a-double-zeros»(Lemma)
  
  Missing owner metadata.
- «prop:a-fourier»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «prop:a-schwartz»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.a
- «prop:a0»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-double-zeros»(Lemma)
  
  Missing owner metadata.
- «prop:b-fourier»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «prop:b-schwartz»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.b
- «prop:b0»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MagicFunction.b.SpecialValues.b_zero
- «prop:ineqA»(Lemma)
  
  Missing owner metadata.
- «prop:ineqB»(Lemma)
  
  Missing owner metadata.
- «theorem:CE_Main»(Theorem)
  
  Missing owner metadata.
- «theorem:psp-density»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-general»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LinearProgrammingBound
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LinearProgrammingBound'
- «thm:Poisson-summation-formula»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- «thm:anti-serre-der-pos»(Theorem)
  
  Missing owner metadata.
- «thm:g1»(Theorem)
  
  Missing owner metadata.
- «thm:g»(Theorem)
  
  Missing owner metadata.
- «thm:periodic-packing-optimal»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - periodic_constant_eq_constant
- «thm:ramanujan-formula»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- «thm:serre-der-modularity»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - serre_D_slash_invariant
- «thm:serre-der-prod-rule»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - serre_D_mul
- «thm:smooth-fast-decay-schwartz»(Theorem)
  
  Missing owner metadata.

Missing effort (111)

E8Packing(Definition)

Missing effort metadata.
Associated lean decls (1)
- E8Packing
IsZLattice(Definition)

Missing effort metadata.
Associated lean decls (1)
- IsZLattice
MainTheorem(Corollary)

Missing effort metadata.
Associated lean decls (1)
- SpherePacking.MainTheorem
PeriodicSpherePacking(Definition)

Missing effort metadata.
Associated lean decls (1)
- PeriodicSpherePacking
SpherePackingConstant(Definition)

Missing effort metadata.
Associated lean decls (1)
- SpherePackingConstant
instDiscreteE8Lattice(Lemma)

Missing effort metadata.
Associated lean decls (1)
- instDiscreteE8Lattice
instLatticeE8(Lemma)

Missing effort metadata.
Associated lean decls (1)
- instIsZLatticeE8Lattice
«E8-Lattice»(Lemma)

Missing effort metadata.
Associated lean decls (1)
- E8Lattice
«E8-Matrix»(Definition)

Missing effort metadata.
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Submodule.E8
Show all 101 more entries missing effort
- «E8-defs-equivalent»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - span_E8Matrix
- «E8-is-basis»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - span_E8Matrix_eq_top
- «E8-vector-norms»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E8_norm_eq_sqrt_even
- «E8Packing-covol»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E8Basis_volume
- «E8Packing-density»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E8Packing_density
- «SpherePacking.balls»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.balls
- «SpherePacking.constant_eq_constant_normalized»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.constant_eq_constant_normalized
- «SpherePacking.density»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.density
- «SpherePacking.finiteDensity»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.finiteDensity
- «SpherePacking.scale_density»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.scale_density
- «SpherePacking.scale_finiteDensity»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «SpherePacking.scale»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SpherePacking.scale
- «cor:MLDE-pos»(Corollary)
  
  Missing effort metadata.
- «cor:disc-nonvanishing»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Δ_ne_zero
- «cor:disc-pos»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Delta_imag_axis_pos
- «cor:ineqAnew»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FG_inequality_1
- «cor:ineqBnew»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FG_inequality_2
- «cor:phi0-bound»(Corollary)
  
  Missing effort metadata.
- «cor:phi0-near-0-infty»(Corollary)
  
  Missing effort metadata.
- «cor:phi2-bound»(Corollary)
  
  Missing effort metadata.
- «cor:phi4-bound»(Corollary)
  
  Missing effort metadata.
- «cor:psiI-near-0-infty»(Corollary)
  
  Missing effort metadata.
- «cor:theta-pos»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - H₂_imag_axis_pos
  - H₄_imag_axis_pos
- «corollary:upper-bound-E8»(Corollary)
  
  Missing effort metadata.
- «def:E2»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E₂_eq
- «def:Ek»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ModularForm.eisensteinSeries_MF
- «def:FG-definition»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - F
  - G
- «def:Fourier-Transform»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Real.fourierIntegral
- «def:H2-H3-H4»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
  - H₂
  - H₃
  - H₄
- «def:Mk»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - ModularForm
- «def:Periodic-sphere-packing-constant»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - PeriodicSpherePackingConstant
- «def:Schwartz-Space»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SchwartzMap
- «def:a-definition»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MagicFunction.a.RealIntegrals.a'
  - MagicFunction.a.RadialFunctions.a
- «def:b-definition»(Definition)
  
  Missing effort metadata.
- «def:dedekind_eta»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - η
- «def:derivative»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - D
- «def:disc-definition»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Δ
- «def:dual-lattice»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LinearMap.BilinForm.dualSubmodule
- «def:h»(Definition)
  
  Missing effort metadata.
- «def:phi4-phi2-phi0»(Definition)
  
  Missing effort metadata.
- «def:psiI-psiT-psiS»(Definition)
  
  Missing effort metadata.
- «def:serre-der»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - serre_D
- «def:slash-operator»(Definition)
  
  Missing effort metadata.
- «def:th00-th01-th10»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
  - Θ₂
  - Θ₃
  - Θ₄
- «lem:bound-I1-I3-I5»(Lemma)
  
  Missing effort metadata.
- «lem:bound-I2-I4-I6»(Lemma)
  
  Missing effort metadata.
- «lem:integral-bound»(Lemma)
  
  Missing effort metadata.
- «lemma:E2-transform-S»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E₂_transform
- «lemma:Ek-Fourier»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - E_k_q_expansion
- «lemma:Ek-is-modular-form»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - EisensteinSeries.eisensteinSeries_SIF
- «lemma:F-G-phi-psi-identities»(Lemma)
  
  Missing effort metadata.
- «lemma:F-G-pos»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «lemma:FG-de»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MLDE_F
  - MLDE_G
- «lemma:Fourier-transform-is-automorphism»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SchwartzMap.fourierTransformCLM
- «lemma:Gaussian-Fourier»(Lemma)
  
  Missing effort metadata.
- «lemma:Qlim»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lemma:Schwartz-summable»(Lemma)
  
  Missing effort metadata.
- «lemma:bound-J1-J3-J5»(Lemma)
  
  Missing effort metadata.
- «lemma:bound-J2-J4-J6»(Lemma)
  
  Missing effort metadata.
- «lemma:disc-cuspform»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Delta
- «lemma:ineqABnew-equiv»(Lemma)
  
  Missing effort metadata.
- «lemma:inv-power-summable»(Lemma)
  
  Missing effort metadata.
- «lemma:jacobi-identity»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - jacobi_identity
- «lemma:lattice-points-bound»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux2_ge'
  - PeriodicSpherePacking.aux2_le'
- «lemma:log-der-inf»(Lemma)
  
  Missing effort metadata.
- «lemma:lv1-lv2-identities»(Lemma)
  
  Missing effort metadata.
- «lemma:mod-div-disc-bound»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
- «lemma:periodic-points-bounds»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux_ge
  - PeriodicSpherePacking.aux_le
- «lemma:phi0-transform»(Lemma)
  
  Missing effort metadata.
- «lemma:psi-bound»(Lemma)
  
  Missing effort metadata.
- «lemma:psi-new»(Lemma)
  
  Missing effort metadata.
- «lemma:psiI-psiT-psiS-fourier»(Lemma)
  
  Missing effort metadata.
- «lemma:slash-negI-even-weight»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - modular_slash_negI_of_even
- «lemma:sp-finite-density-bound»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - SpherePacking.finiteDensity_le
  - SpherePacking.finiteDensity_ge
- «lemma:theta-modular»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lemma:theta-transform-S-T»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lemma:volume-ball-ratio-limit»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «prop:Qdec»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FmodG_strictAntiOn
- «prop:a-double-zeros»(Lemma)
  
  Missing effort metadata.
- «prop:a-fourier»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «prop:a-schwartz»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.a
- «prop:a0»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-double-zeros»(Lemma)
  
  Missing effort metadata.
- «prop:b-fourier»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «prop:b-schwartz»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.b
- «prop:b0»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MagicFunction.b.SpecialValues.b_zero
- «prop:ineqA»(Lemma)
  
  Missing effort metadata.
- «prop:ineqB»(Lemma)
  
  Missing effort metadata.
- «theorem:CE_Main»(Theorem)
  
  Missing effort metadata.
- «theorem:psp-density»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-general»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LinearProgrammingBound
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LinearProgrammingBound'
- «thm:Poisson-summation-formula»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- «thm:anti-serre-der-pos»(Theorem)
  
  Missing effort metadata.
- «thm:g1»(Theorem)
  
  Missing effort metadata.
- «thm:g»(Theorem)
  
  Missing effort metadata.
- «thm:periodic-packing-optimal»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - periodic_constant_eq_constant
- «thm:ramanujan-formula»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- «thm:serre-der-modularity»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - serre_D_slash_invariant
- «thm:serre-der-prod-rule»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - serre_D_mul
- «thm:smooth-fast-decay-schwartz»(Theorem)
  
  Missing effort metadata.

Untagged (111)

E8Packing(Definition)

Missing tag metadata.
Associated lean decls (1)
- E8Packing
IsZLattice(Definition)

Missing tag metadata.
Associated lean decls (1)
- IsZLattice
MainTheorem(Corollary)

Missing tag metadata.
Associated lean decls (1)
- SpherePacking.MainTheorem
PeriodicSpherePacking(Definition)

Missing tag metadata.
Associated lean decls (1)
- PeriodicSpherePacking
SpherePackingConstant(Definition)

Missing tag metadata.
Associated lean decls (1)
- SpherePackingConstant
instDiscreteE8Lattice(Lemma)

Missing tag metadata.
Associated lean decls (1)
- instDiscreteE8Lattice
instLatticeE8(Lemma)

Missing tag metadata.
Associated lean decls (1)
- instIsZLatticeE8Lattice
«E8-Lattice»(Lemma)

Missing tag metadata.
Associated lean decls (1)
- E8Lattice
«E8-Matrix»(Definition)

Missing tag metadata.
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Submodule.E8
Show all 101 more untagged entries
- «E8-defs-equivalent»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - span_E8Matrix
- «E8-is-basis»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - span_E8Matrix_eq_top
- «E8-vector-norms»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E8_norm_eq_sqrt_even
- «E8Packing-covol»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E8Basis_volume
- «E8Packing-density»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E8Packing_density
- «SpherePacking.balls»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.balls
- «SpherePacking.constant_eq_constant_normalized»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.constant_eq_constant_normalized
- «SpherePacking.density»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.density
- «SpherePacking.finiteDensity»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.finiteDensity
- «SpherePacking.scale_density»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.scale_density
- «SpherePacking.scale_finiteDensity»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «SpherePacking.scale»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SpherePacking.scale
- «cor:MLDE-pos»(Corollary)
  
  Missing tag metadata.
- «cor:disc-nonvanishing»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Δ_ne_zero
- «cor:disc-pos»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Delta_imag_axis_pos
- «cor:ineqAnew»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FG_inequality_1
- «cor:ineqBnew»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FG_inequality_2
- «cor:phi0-bound»(Corollary)
  
  Missing tag metadata.
- «cor:phi0-near-0-infty»(Corollary)
  
  Missing tag metadata.
- «cor:phi2-bound»(Corollary)
  
  Missing tag metadata.
- «cor:phi4-bound»(Corollary)
  
  Missing tag metadata.
- «cor:psiI-near-0-infty»(Corollary)
  
  Missing tag metadata.
- «cor:theta-pos»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - H₂_imag_axis_pos
  - H₄_imag_axis_pos
- «corollary:upper-bound-E8»(Corollary)
  
  Missing tag metadata.
- «def:E2»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E₂_eq
- «def:Ek»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ModularForm.eisensteinSeries_MF
- «def:FG-definition»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - F
  - G
- «def:Fourier-Transform»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Real.fourierIntegral
- «def:H2-H3-H4»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
  - H₂
  - H₃
  - H₄
- «def:Mk»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - ModularForm
- «def:Periodic-sphere-packing-constant»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - PeriodicSpherePackingConstant
- «def:Schwartz-Space»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SchwartzMap
- «def:a-definition»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MagicFunction.a.RealIntegrals.a'
  - MagicFunction.a.RadialFunctions.a
- «def:b-definition»(Definition)
  
  Missing tag metadata.
- «def:dedekind_eta»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - η
- «def:derivative»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - D
- «def:disc-definition»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Δ
- «def:dual-lattice»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LinearMap.BilinForm.dualSubmodule
- «def:h»(Definition)
  
  Missing tag metadata.
- «def:phi4-phi2-phi0»(Definition)
  
  Missing tag metadata.
- «def:psiI-psiT-psiS»(Definition)
  
  Missing tag metadata.
- «def:serre-der»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - serre_D
- «def:slash-operator»(Definition)
  
  Missing tag metadata.
- «def:th00-th01-th10»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
  - Θ₂
  - Θ₃
  - Θ₄
- «lem:bound-I1-I3-I5»(Lemma)
  
  Missing tag metadata.
- «lem:bound-I2-I4-I6»(Lemma)
  
  Missing tag metadata.
- «lem:integral-bound»(Lemma)
  
  Missing tag metadata.
- «lemma:E2-transform-S»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E₂_transform
- «lemma:Ek-Fourier»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - E_k_q_expansion
- «lemma:Ek-is-modular-form»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - EisensteinSeries.eisensteinSeries_SIF
- «lemma:F-G-phi-psi-identities»(Lemma)
  
  Missing tag metadata.
- «lemma:F-G-pos»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «lemma:FG-de»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MLDE_F
  - MLDE_G
- «lemma:Fourier-transform-is-automorphism»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SchwartzMap.fourierTransformCLM
- «lemma:Gaussian-Fourier»(Lemma)
  
  Missing tag metadata.
- «lemma:Qlim»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lemma:Schwartz-summable»(Lemma)
  
  Missing tag metadata.
- «lemma:bound-J1-J3-J5»(Lemma)
  
  Missing tag metadata.
- «lemma:bound-J2-J4-J6»(Lemma)
  
  Missing tag metadata.
- «lemma:disc-cuspform»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Delta
- «lemma:ineqABnew-equiv»(Lemma)
  
  Missing tag metadata.
- «lemma:inv-power-summable»(Lemma)
  
  Missing tag metadata.
- «lemma:jacobi-identity»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - jacobi_identity
- «lemma:lattice-points-bound»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux2_ge'
  - PeriodicSpherePacking.aux2_le'
- «lemma:log-der-inf»(Lemma)
  
  Missing tag metadata.
- «lemma:lv1-lv2-identities»(Lemma)
  
  Missing tag metadata.
- «lemma:mod-div-disc-bound»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
- «lemma:periodic-points-bounds»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - PeriodicSpherePacking.aux_ge
  - PeriodicSpherePacking.aux_le
- «lemma:phi0-transform»(Lemma)
  
  Missing tag metadata.
- «lemma:psi-bound»(Lemma)
  
  Missing tag metadata.
- «lemma:psi-new»(Lemma)
  
  Missing tag metadata.
- «lemma:psiI-psiT-psiS-fourier»(Lemma)
  
  Missing tag metadata.
- «lemma:slash-negI-even-weight»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - modular_slash_negI_of_even
- «lemma:sp-finite-density-bound»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - SpherePacking.finiteDensity_le
  - SpherePacking.finiteDensity_ge
- «lemma:theta-modular»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lemma:theta-transform-S-T»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lemma:volume-ball-ratio-limit»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «prop:Qdec»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FmodG_strictAntiOn
- «prop:a-double-zeros»(Lemma)
  
  Missing tag metadata.
- «prop:a-fourier»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «prop:a-schwartz»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.a
- «prop:a0»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-double-zeros»(Lemma)
  
  Missing tag metadata.
- «prop:b-fourier»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «prop:b-schwartz»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.b
- «prop:b0»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MagicFunction.b.SpecialValues.b_zero
- «prop:ineqA»(Lemma)
  
  Missing tag metadata.
- «prop:ineqB»(Lemma)
  
  Missing tag metadata.
- «theorem:CE_Main»(Theorem)
  
  Missing tag metadata.
- «theorem:psp-density»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-general»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LinearProgrammingBound
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LinearProgrammingBound'
- «thm:Poisson-summation-formula»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- «thm:anti-serre-der-pos»(Theorem)
  
  Missing tag metadata.
- «thm:g1»(Theorem)
  
  Missing tag metadata.
- «thm:g»(Theorem)
  
  Missing tag metadata.
- «thm:periodic-packing-optimal»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - periodic_constant_eq_constant
- «thm:ramanujan-formula»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- «thm:serre-der-modularity»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - serre_D_slash_invariant
- «thm:serre-der-prod-rule»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - serre_D_mul
- «thm:smooth-fast-decay-schwartz»(Theorem)
  
  Missing tag metadata.

Structure and coverage

Informal-only37Statements with no associated Lean code yet.

Ready to formalize74Entries whose next step is currently unblocked.

Heaviest prerequisites (33)

«thm:g1»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 0proof deps: 8direct uses: 1downstream unlocks: 1
«cor:phi0-near-0-infty»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 0proof deps: 3direct uses: 0downstream unlocks: 0
«prop:Qdec»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- FmodG_strictAntiOn
«E8Packing-density»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- E8Packing_density
«cor:MLDE-pos»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 2
«corollary:upper-bound-E8»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 1
«lemma:FG-de»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
Associated lean decls (2)
- MLDE_F
- MLDE_G
«thm:Cohn-Elkies-general»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- LinearProgrammingBound
«thm:anti-serre-der-pos»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 3
MainTheorem(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- SpherePacking.MainTheorem
Show all 23 more heaviest-prerequisite entries
- «E8-Lattice»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - E8Lattice
- «SpherePacking.constant_eq_constant_normalized»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - SpherePacking.constant_eq_constant_normalized
- «SpherePacking.scale_density»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - SpherePacking.scale_density
- «cor:ineqAnew»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - FG_inequality_1
- «cor:ineqBnew»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - FG_inequality_2
- «cor:phi0-bound»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 3downstream unlocks: 3
- «cor:phi2-bound»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
- «cor:phi4-bound»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
- «cor:psiI-near-0-infty»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 3
- «lem:bound-I1-I3-I5»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lem:bound-I2-I4-I6»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lemma:Schwartz-summable»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lemma:bound-J1-J3-J5»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lemma:bound-J2-J4-J6»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lemma:ineqABnew-equiv»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «lemma:psiI-psiT-psiS-fourier»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «prop:a-schwartz»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.a
- «prop:b-double-zeros»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 2
- «prop:b-schwartz»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.b
- «theorem:psp-density»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - PeriodicSpherePacking.density_eq
- «thm:Cohn-Elkies-periodic»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LinearProgrammingBound'
- «thm:g»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
- «thm:ramanujan-formula»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 4
  Associated lean decls (6)

No prerequisites (78)

«lemma:Ek-Fourier»(Lemma)
Associated lean decls (1)
- E_k_q_expansion
«prop:b0»(Lemma)
Associated lean decls (1)
- MagicFunction.b.SpecialValues.b_zero
«lemma:theta-transform-S-T»(Lemma)
Associated lean decls (6)
«def:Fourier-Transform»(Definition)
Associated lean decls (1)
- Real.fourierIntegral
«def:dedekind_eta»(Definition)
Associated lean decls (1)
- η
«prop:a-double-zeros»(Lemma)
«thm:periodic-packing-optimal»(Theorem)
Associated lean decls (1)
- periodic_constant_eq_constant
«SpherePacking.scale»(Definition)
Associated lean decls (1)
- SpherePacking.scale
«thm:serre-der-modularity»(Theorem)
Associated lean decls (1)
- serre_D_slash_invariant
«def:Periodic-sphere-packing-constant»(Definition)
Associated lean decls (1)
- PeriodicSpherePackingConstant
Show all 68 more entries without prerequisites
- «prop:ineqB»(Lemma)
- «lemma:Qlim»(Lemma)
  Associated lean decls (1)
  - FmodG_rightLimitAt_zero
- «lem:integral-bound»(Lemma)
- E8Packing(Definition)
  Associated lean decls (1)
  - E8Packing
- PeriodicSpherePacking(Definition)
  Associated lean decls (1)
  - PeriodicSpherePacking
- «E8-Matrix»(Definition)
  Associated lean decls (1)
  - E8Matrix
- «E8-Set»(Definition)
  Associated lean decls (1)
  - Submodule.E8
- «SpherePacking.density»(Definition)
  Associated lean decls (1)
  - SpherePacking.density
- «def:dual-lattice»(Definition)
  Associated lean decls (1)
  - LinearMap.BilinForm.dualSubmodule
- «lemma:jacobi-identity»(Lemma)
  Associated lean decls (1)
  - jacobi_identity
- instDiscreteE8Lattice(Lemma)
  Associated lean decls (1)
  - instDiscreteE8Lattice
- «lemma:psi-new»(Lemma)
- «def:Ek»(Definition)
  Associated lean decls (1)
  - ModularForm.eisensteinSeries_MF
- «def:Schwartz-Space»(Definition)
  Associated lean decls (1)
  - SchwartzMap
- «lemma:phi0-transform»(Lemma)
- «lemma:volume-ball-ratio-limit»(Lemma)
  Associated lean decls (1)
  - volume_ball_ratio_tendsto_nhds_one''
- «lemma:lattice-points-bound»(Lemma)
  Associated lean decls (2)
  - PeriodicSpherePacking.aux2_ge'
  - PeriodicSpherePacking.aux2_le'
- «lemma:sp-finite-density-bound»(Lemma)
  Associated lean decls (2)
  - SpherePacking.finiteDensity_le
  - SpherePacking.finiteDensity_ge
- «def:phi4-phi2-phi0»(Definition)
- «cor:disc-nonvanishing»(Corollary)
  Associated lean decls (1)
  - Δ_ne_zero
- «lemma:psi-bound»(Lemma)
- «lemma:F-G-phi-psi-identities»(Lemma)
- «E8-vector-norms»(Lemma)
  Associated lean decls (1)
  - E8_norm_eq_sqrt_even
- «SpherePacking.scale_finiteDensity»(Lemma)
  Associated lean decls (1)
  - SpherePacking.scale_finiteDensity
- «lemma:periodic-points-bounds»(Lemma)
  Associated lean decls (2)
  - PeriodicSpherePacking.aux_ge
  - PeriodicSpherePacking.aux_le
- «lemma:inv-power-summable»(Lemma)
- «lemma:slash-negI-even-weight»(Lemma)
  Associated lean decls (1)
  - modular_slash_negI_of_even
- «lemma:log-der-inf»(Lemma)
- «def:E2»(Definition)
  Associated lean decls (1)
  - E₂_eq
- «cor:theta-pos»(Corollary)
  Associated lean decls (2)
  - H₂_imag_axis_pos
  - H₄_imag_axis_pos
- «lemma:disc-cuspform»(Lemma)
  Associated lean decls (1)
  - Delta
- «def:b-definition»(Definition)
- «def:th00-th01-th10»(Definition)
  Associated lean decls (3)
  - Θ₂
  - Θ₃
  - Θ₄
- «E8-defs-equivalent»(Theorem)
  Associated lean decls (1)
  - span_E8Matrix
- «E8Packing-covol»(Lemma)
  Associated lean decls (1)
  - E8Basis_volume
- «thm:serre-der-prod-rule»(Theorem)
  Associated lean decls (1)
  - serre_D_mul
- «SpherePacking.finiteDensity»(Definition)
  Associated lean decls (1)
  - SpherePacking.finiteDensity
- «lemma:Gaussian-Fourier»(Lemma)
- IsZLattice(Definition)
  Associated lean decls (1)
  - IsZLattice
- «lemma:Ek-is-modular-form»(Lemma)
  Associated lean decls (1)
  - EisensteinSeries.eisensteinSeries_SIF
- «def:Mk»(Definition)
  Associated lean decls (1)
  - ModularForm
- «def:derivative»(Definition)
  Associated lean decls (1)
  - D
- «SpherePacking.balls»(Definition)
  Associated lean decls (1)
  - SpherePacking.balls
- «thm:smooth-fast-decay-schwartz»(Theorem)
- «lemma:E2-transform-S»(Lemma)
  Associated lean decls (1)
  - E₂_transform
- «def:serre-der»(Definition)
  Associated lean decls (1)
  - serre_D
- «theorem:CE_Main»(Theorem)
- «cor:disc-pos»(Corollary)
  Associated lean decls (1)
  - Delta_imag_axis_pos
- «def:H2-H3-H4»(Definition)
  Associated lean decls (3)
  - H₂
  - H₃
  - H₄
- «prop:a-fourier»(Lemma)
  Associated lean decls (1)
  - MagicFunction.a.Fourier.eig_a
- «lemma:mod-div-disc-bound»(Lemma)
  Associated lean decls (1)
  - MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff
- «def:FG-definition»(Definition)
  Associated lean decls (2)
  - F
  - G
- «def:psiI-psiT-psiS»(Definition)
- «prop:a0»(Lemma)
  Associated lean decls (1)
  - MagicFunction.a.SpecialValues.a_zero
- «prop:b-fourier»(Lemma)
  Associated lean decls (1)
  - MagicFunction.b.Fourier.eig_b
- «E8-is-basis»(Lemma)
  Associated lean decls (1)
  - span_E8Matrix_eq_top
- «lemma:F-G-pos»(Lemma)
  Associated lean decls (2)
  - F_imag_axis_pos
  - G_imag_axis_pos
- «def:slash-operator»(Definition)
- «def:h»(Definition)
- «def:disc-definition»(Definition)
  Associated lean decls (1)
  - Δ
- «lemma:Fourier-transform-is-automorphism»(Lemma)
  Associated lean decls (1)
  - SchwartzMap.fourierTransformCLM
- SpherePackingConstant(Definition)
  Associated lean decls (1)
  - SpherePackingConstant
- «lemma:lv1-lv2-identities»(Lemma)
- «thm:Poisson-summation-formula»(Theorem)
  Associated lean decls (1)
  - SchwartzMap.PoissonSummation_Lattices
- instLatticeE8(Lemma)
  Associated lean decls (1)
  - instIsZLatticeE8Lattice
- «prop:ineqA»(Lemma)
- «lemma:theta-modular»(Lemma)
  Associated lean decls (3)
- «def:a-definition»(Definition)
  Associated lean decls (2)
  - MagicFunction.a.RealIntegrals.a'
  - MagicFunction.a.RadialFunctions.a

No dependents (68)

«lemma:Ek-Fourier»(Lemma)
Associated lean decls (1)
- E_k_q_expansion
«def:Periodic-sphere-packing-constant»(Definition)
Associated lean decls (1)
- PeriodicSpherePackingConstant
PeriodicSpherePacking(Definition)
Associated lean decls (1)
- PeriodicSpherePacking
«cor:ineqAnew»(Corollary)
Associated lean decls (1)
- FG_inequality_1
«prop:b-schwartz»(Lemma)
Associated lean decls (1)
- MagicFunction.FourierEigenfunctions.b
«E8-Matrix»(Definition)
Associated lean decls (1)
- E8Matrix
«E8-Set»(Definition)
Associated lean decls (1)
- Submodule.E8
«cor:phi0-near-0-infty»(Corollary)
«SpherePacking.density»(Definition)
Associated lean decls (1)
- SpherePacking.density
«def:dual-lattice»(Definition)
Associated lean decls (1)
- LinearMap.BilinForm.dualSubmodule
Show all 58 more entries without dependents
- «lemma:bound-J1-J3-J5»(Lemma)
- «def:h»(Definition)
- «E8-Lattice»(Lemma)
  Associated lean decls (1)
  - E8Lattice
- «lemma:ineqABnew-equiv»(Lemma)
- «SpherePacking.constant_eq_constant_normalized»(Lemma)
  Associated lean decls (1)
  - SpherePacking.constant_eq_constant_normalized
- «lemma:jacobi-identity»(Lemma)
  Associated lean decls (1)
  - jacobi_identity
- «def:Ek»(Definition)
  Associated lean decls (1)
  - ModularForm.eisensteinSeries_MF
- «def:Schwartz-Space»(Definition)
  Associated lean decls (1)
  - SchwartzMap
- «lemma:phi0-transform»(Lemma)
- «thm:Cohn-Elkies-general»(Theorem)
  Associated lean decls (1)
  - LinearProgrammingBound
- «E8-is-basis»(Lemma)
  Associated lean decls (1)
  - span_E8Matrix_eq_top
- «lemma:lattice-points-bound»(Lemma)
  Associated lean decls (2)
  - PeriodicSpherePacking.aux2_ge'
  - PeriodicSpherePacking.aux2_le'
- «lemma:sp-finite-density-bound»(Lemma)
  Associated lean decls (2)
  - SpherePacking.finiteDensity_le
  - SpherePacking.finiteDensity_ge
- «def:H2-H3-H4»(Definition)
  Associated lean decls (3)
  - H₂
  - H₃
  - H₄
- «lemma:Schwartz-summable»(Lemma)
- «lemma:periodic-points-bounds»(Lemma)
  Associated lean decls (2)
  - PeriodicSpherePacking.aux_ge
  - PeriodicSpherePacking.aux_le
- «def:E2»(Definition)
  Associated lean decls (1)
  - E₂_eq
- «SpherePacking.finiteDensity»(Definition)
  Associated lean decls (1)
  - SpherePacking.finiteDensity
- «lemma:Gaussian-Fourier»(Lemma)
- IsZLattice(Definition)
  Associated lean decls (1)
  - IsZLattice
- «lemma:Ek-is-modular-form»(Lemma)
  Associated lean decls (1)
  - EisensteinSeries.eisensteinSeries_SIF
- «def:Mk»(Definition)
  Associated lean decls (1)
  - ModularForm
- «def:derivative»(Definition)
  Associated lean decls (1)
  - D
- «SpherePacking.balls»(Definition)
  Associated lean decls (1)
  - SpherePacking.balls
- «lemma:E2-transform-S»(Lemma)
  Associated lean decls (1)
  - E₂_transform
- «lemma:bound-J2-J4-J6»(Lemma)
- «lem:bound-I2-I4-I6»(Lemma)
- «def:serre-der»(Definition)
  Associated lean decls (1)
  - serre_D
- «prop:a-schwartz»(Lemma)
  Associated lean decls (1)
  - MagicFunction.FourierEigenfunctions.a
- «def:th00-th01-th10»(Definition)
  Associated lean decls (3)
  - Θ₂
  - Θ₃
  - Θ₄
- «def:b-definition»(Definition)
- «lemma:disc-cuspform»(Lemma)
  Associated lean decls (1)
  - Delta
- «lemma:slash-negI-even-weight»(Lemma)
  Associated lean decls (1)
  - modular_slash_negI_of_even
- «E8-vector-norms»(Lemma)
  Associated lean decls (1)
  - E8_norm_eq_sqrt_even
- «cor:ineqBnew»(Corollary)
  Associated lean decls (1)
  - FG_inequality_2
- «thm:g»(Theorem)
- «def:FG-definition»(Definition)
  Associated lean decls (2)
  - F
  - G
- «E8Packing-density»(Theorem)
  Associated lean decls (1)
  - E8Packing_density
- «cor:disc-nonvanishing»(Corollary)
  Associated lean decls (1)
  - Δ_ne_zero
- «lem:bound-I1-I3-I5»(Lemma)
- «def:psiI-psiT-psiS»(Definition)
- «def:phi4-phi2-phi0»(Definition)
- instDiscreteE8Lattice(Lemma)
  Associated lean decls (1)
  - instDiscreteE8Lattice
- «def:slash-operator»(Definition)
- «def:disc-definition»(Definition)
  Associated lean decls (1)
  - Δ
- «lemma:Fourier-transform-is-automorphism»(Lemma)
  Associated lean decls (1)
  - SchwartzMap.fourierTransformCLM
- SpherePackingConstant(Definition)
  Associated lean decls (1)
  - SpherePackingConstant
- «lemma:lv1-lv2-identities»(Lemma)
- instLatticeE8(Lemma)
  Associated lean decls (1)
  - instIsZLatticeE8Lattice
- E8Packing(Definition)
  Associated lean decls (1)
  - E8Packing
- «SpherePacking.scale»(Definition)
  Associated lean decls (1)
  - SpherePacking.scale
- «def:dedekind_eta»(Definition)
  Associated lean decls (1)
  - η
- «def:Fourier-Transform»(Definition)
  Associated lean decls (1)
  - Real.fourierIntegral
- «lemma:theta-transform-S-T»(Lemma)
  Associated lean decls (6)
- MainTheorem(Corollary)
  Associated lean decls (1)
  - SpherePacking.MainTheorem
- «lemma:theta-modular»(Lemma)
  Associated lean decls (3)
- «def:a-definition»(Definition)
  Associated lean decls (2)
  - MagicFunction.a.RealIntegrals.a'
  - MagicFunction.a.RadialFunctions.a
- «lemma:psiI-psiT-psiS-fourier»(Lemma)

Proof debt hotspots (23)

Theta constants and identities used in the magic-function construction.theta_and_identities

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 6incomplete decls: 18missing decls: 0total debt: 18
Eisenstein series, the discriminant form, and positivity/nonvanishing tools.eisenstein_discriminant

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 10incomplete decls: 10missing decls: 0total debt: 10
Serre derivative identities and differential inequalities.serre_derivative

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 5incomplete decls: 10missing decls: 0total debt: 10
Basic structural and arithmetic properties of <missing> .e8_properties

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 5incomplete decls: 5missing decls: 0total debt: 5
Periodic and lattice packings as a reduced optimization class.periodic_packings

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 5incomplete decls: 5missing decls: 0total debt: 5
Differential equations and monotonicity control.fg_differential

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 4incomplete decls: 5missing decls: 0total debt: 5
Auxiliary functions <missing> and reformulation of inequalities.fg_setup

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 3incomplete decls: 5missing decls: 0total debt: 5
Volume-count asymptotics for lattice and periodic center sets.density_periodic_counts

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 3incomplete decls: 5missing decls: 0total debt: 5
Definitions of sphere packings, density, and the optimization target.sphere_setup

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 4incomplete decls: 4missing decls: 0total debt: 4
Scaling invariance of finite density and asymptotic density.sphere_scaling

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 4incomplete decls: 4missing decls: 0total debt: 4
Show all 13 more proof-debt hotspots
- Definition and density computation of the <missing> sphere packing.e8_density
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 3incomplete decls: 3missing decls: 0total debt: 3
- Equivalent models of the <missing> lattice.e8_definitions
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 3incomplete decls: 3missing decls: 0total debt: 3
- Fourier transform and Schwartz-space preliminaries.fourier_setup
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 3incomplete decls: 3missing decls: 0total debt: 3
- Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .magic_a_properties
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 3incomplete decls: 3missing decls: 0total debt: 3
- Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .magic_b_properties
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 3incomplete decls: 3missing decls: 0total debt: 3
- Auxiliary modular expressions and integral formulas defining <missing> .magic_phi_construction
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 2incomplete decls: 3missing decls: 0total debt: 3
- Congruence groups, slash operators, and modular forms.modular_forms_setup
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 2incomplete decls: 2missing decls: 0total debt: 2
- Bounds comparing finite density with local center counts.density_finite_bounds
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 2missing decls: 0total debt: 2
- Closed formula for density of periodic sphere packings.density_formula
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
- Linear programming bound for periodic sphere packings.ce_periodic
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
- Passage from periodic to general packings.ce_general
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
- Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.sphere_main_statement
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
- Summability lemmas and Poisson summation over lattices.poisson_formula
  
  Grouped proof/code debt derived from the current incomplete-declaration snapshots.
  
  affected entries: 1incomplete decls: 1missing decls: 0total debt: 1