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 filterssigma_qexp_deriv_bound_generic
Plain-language statement
Generic derivative bound for σ_k q-series on compact sets. Uses σ_k(n) ≤ n^(k+1) (sigma_bound) and iter_deriv_comp_bound3 for exponential decay.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
sigma_qexp_summable_generic
Plain-language statement
Generic summability for n^a * σ_b(n) * exp(2πinz) series. Uses σ_b(n) ≤ n^(b+1) (sigma_bound) and a33 (a+b+1) for exponential summability.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Δ_fun_eq_Δ
Plain-language statement
The discriminant Δ_fun = 1728⁻¹(E₄³ - E₆²) equals the standard discriminant Δ.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.