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 101 research declarations. Search 10,000 more complete Mathlib declarations.
101 results
Clear filtersE₂_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.
E₄_eq_H_sum_sq
Plain-language statement
E₄.toFun = H₂² + H₂H₄ + H₄². Both are weight-4 level-1 modular forms tending to 1 at ∞, so their difference is a weight-4 cusp form, hence zero.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₄_sigma_qexp
Plain-language statement
E₄ as explicit tsum (from E4_q_exp PowerSeries coefficients). Uses hasSum_qExpansion to convert from PowerSeries to tsum form.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.