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 filtersD_cexp_div
Plain-language statement
D(exp(cz))/exp(cz) = c/(2πi) for any coefficient c.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
D_diff_qexp
Plain-language statement
D(E₂E₄ - E₆) = 720 * ∑ n²·σ₃(n)·qⁿ. Key for the log-derivative limit: (D F)/F → 2 as z → i∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_imag_axis_re_pos
Plain-language statement
The real part of (D E₄)(it) is positive for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_qexp
Plain-language statement
D E₄ q-expansion via termwise differentiation. D E₄ = 240 * ∑ n * σ₃(n) * qⁿ from differentiating E₄ = 1 + 240 * ∑ σ₃(n) * qⁿ.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_term_re_pos
Plain-language statement
Each term n*σ₃(n)*exp(-2πnt) in D E₄ q-expansion has positive real part on imaginary axis.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_FmodGReal
Plain-language statement
The derivative of FmodGReal is (-2π) * L₁,₀(it) / G(it)².
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.