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 27 research declarations. Search 10,000 more complete Mathlib declarations.
27 results
Clear filtersE₂_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₂_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₂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₄_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.
F_functional_equation
Project documentation
Reduce a power of I * w via I ^ 4 = 1. -/ lemma I_mul_npow (w : ℂ) (n : ℕ) : (I * w) ^ n = I ^ (n % 4) * w ^ n := by rw [mul_pow, I_pow_eq_pow_mod] /- Functional equation of
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
F_functional_equation'
Plain-language statement
Functional equation of restricted to the imaginary axis.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.