Source-pinned research
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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersE₂_isBoundedAtImInfty
Plain-language 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π))³.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_mul_E₄_sub_E₆
Plain-language 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).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_S_transform
Plain-language statement
E₂ transforms under S as: E₂(-1/z) = z² · (E₂(z) + 6/(πIz)).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_sigma_qexp
Plain-language 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.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_sub_one_isBigO_exp
Plain-language statement
E₂ - 1 = O(exp(-2π·Im z)) at infinity.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂E₄_sub_E₆_div_q_tendsto
Plain-language statement
(E₂E₄ - E₆) / q → 720 as im(z) → ∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.