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 filtersG_vanishing_order
Plain-language statement
G / q^(3/2) → 20480 as im(z) → ∞. Here q^(3/2) = exp(2πi · (3/2) · z).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
L₁₀_div_FG_tendsto
Plain-language statement
lim_{t→∞} L₁,₀(it)/(F(it)G(it)) = 1/2.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
logderiv_tendsto_of_div_exp_tendsto
Plain-language statement
If F z / exp(a·z) → C ≠ 0 at i∞, then D F / F → a/(2πi): the exponential contributes a/(2πi) and the bounded limit factor's log-derivative vanishes. Public so downstream files (e.g. #331's Θ₂ analysis) can reuse it.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
negDE₂_imag_axis_re_pos
Plain-language statement
The real part of negDE₂(it) is positive for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
negDE₂_qexp
Plain-language statement
Q-expansion identity: negDE₂ = 24 * ∑ n * σ₁(n) * q^n From Ramanujan's formula: D E₂ = (E₂² - E₄)/12, so -D E₂ = (E₄ - E₂²)/12. And the derivative of E₂ = 1 - 24∑ σ₁(n) q^n gives -D E₂ = 24 ∑ n σ₁(n) q^n. See blueprint equation at line 136 of modform-ineq.tex. Proof outline: 1. E₂_sigma_qexp: E₂ = 1 - 24 * ∑ σ₁(n) * q^n 2. D_qexp_tsum_pnat: D(∑ a(n) * q^n...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
negDE₂_term_re_pos
Plain-language statement
Each term n*σ₁(n)*exp(-2πnt) in the q-expansion of negDE₂ has positive real part.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.