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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersSpherePacking.inter_ball_encard_le
Plain-language statement
This gives an upper bound on the number of points in the sphere packing X with norm less than R.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.scale_density
Plain-language statement
Density of a scaled packing.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.scale_finiteDensity
Plain-language statement
Finite density of a scaled packing.
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.
tendsto_resToImagAxis_of_tendsto_atImInfty
Plain-language statement
Tendsto conversion: if F tends to c at atImInfty, then F.resToImagAxis tends to c at atTop.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
tendsto_rpow_mul_of_isBigO_exp
Project documentation
The analytic kernel: if g : ℝ → ℂ is eventually bounded by C * exp(-b * t) for some b > 0, then t^s * g(t) → 0 as t → ∞ for any real power s. This follows from the fact that t^s * exp(-b * t) → 0 (mathlib's tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero) combined with the big-O transfer lemma.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.