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 8 research declarations. Search 10,000 more complete Mathlib declarations.
8 results
Clear filterstendsto_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.