Project-declaredLean 4.31.0
E₂ imag axis real
E₂_imag_axis_real
Mathematical statement
E₂(it) is real for all t > 0.
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Source-pinned research
Research proof index
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 907 to 912 of 2,569 results.
View proof record
Project-declaredLean 4.31.0
E₂ is Bounded At Im Infty
E₂_isBoundedAtImInfty
Mathematical statement
E₂ is bounded at infinity. Uses E₂_eq: E₂(z) = 1 - 24·Σₙ₌₁ n·qⁿ/(1-qⁿ) where q = exp(2πiz). For im(z) ≥ 1, |q| ≤ exp(-2π), so by norm_tsum_logDeriv_expo_le, |E₂| ≤ 1 + 24·exp(-2π)/(1-exp(-2π))³.
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Project-declaredLean 4.31.0
E₂ mul E₄ sub E₆
E₂_mul_E₄_sub_E₆
Mathematical statement
The q-expansion identity E₂E₄ - E₆ = 720·Σn·σ₃(n)·qⁿ. This follows from Ramanujan's formula: E₂E₄ - E₆ = 3·D(E₄), combined with D(E₄) = 240·Σn·σ₃(n)·qⁿ (since D multiplies q-coefficients by n).
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Project-declaredLean 4.31.0
E₂ S transform
E₂_S_transform
Mathematical statement
E₂ transforms under S as: E₂(-1/z) = z² · (E₂(z) + 6/(πIz)).
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Project-declaredLean 4.31.0
E₂ sigma qexp
E₂_sigma_qexp
Mathematical statement
E₂ q-expansion in sigma form: E₂ = 1 - 24 * ∑ σ₁(n) * q^n. This follows from G2_q_exp and the definition E₂ = (1/(2*ζ(2))) • G₂. The proof expands the definitions and simplifies using ζ(2) = π²/6.
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Project-declaredLean 4.31.0
E₂ sub one is Big O exp
E₂_sub_one_isBigO_exp
Mathematical statement
E₂ - 1 = O(exp(-2π·Im z)) at infinity.
sphere packingFourier analysismodular forms
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.