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 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersE₂_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.
modular_form_tendsto_atImInfty
Plain-language statement
A modular form tends to its value at infinity as z → i∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
qexp_deriv_bound_of_coeff_bound
Plain-language statement
Derivative bounds for q-expansion coefficients. Given ‖a n‖ ≤ n^k, produces bounds ‖a n * 2πin * exp(2πin z)‖ ≤ 2π * n^(k+1) * exp(-2πn * y_min) on compact K ⊆ {z : 0 < z.im}. This is a key hypothesis for D_qexp_tsum_pnat.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
serre_D_tendsto_of_tendsto
Project documentation
General limit: if f → c at i∞ and f is holomorphic and bounded, then serre_D k f → -k*c/12. This is the continuous mapping theorem applied to serre_D k f = D f - (k/12) * E₂ * f: - D f → 0 (Cauchy estimate from boundedness) - E₂ → 1 - f → c Therefore serre_D k f → 0 - (k/12) * 1 * c = -k*c/12.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
summable_pow_shift
Plain-language statement
Summability of (m+1)^k * exp(-2πm) via comparison with shifted sum.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.