Source-pinned research

Research proof index

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 101 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

101 results

Clear filters
Project-declaredLean 4.31.0

F₄ tendsto at Im Infty

f₄_tendsto_atImInfty

Plain-language statement

f₄ tends to 0 at infinity. Proof: f₄ = serre_D 2 H₄ + (1/6)H₄(2H₂ + H₄) serre_D 2 H₄ = D H₄ - (1/6)E₂ H₄ → 0 - (1/6)11 = -1/6 (since H₄ → 1, E₂ → 1) H₄(2H₂ + H₄) → 1*(0 + 1) = 1 So f₄ → -1/6 + (1/6)*1 = 0.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Fmod G right Limit At zero

FmodG_rightLimitAt_zero

Plain-language statement

limt0+F(it)/G(it)=18/π2\lim_{t \to 0^+} F(it) / G(it) = 18 / \pi^2. Proof outline (following blueprint Lemma 8.8): 1. Change of variables: lim_{t→0⁺} F(it)/G(it) = lim_{s→∞} F(i/s)/G(i/s) 2. Apply functional equations: - F(i/s) = s^12F(is) - 12s^11/πF₁(is)E₄(is) + 36s^10/π²E₄(is)² - G(i/s) = s^10H₄(is)³(2H₄(is)² + 5H₄(is)*H₂(is) + 5H₂(is)²) 3. Divide to get: F(i/s)/G(i/...

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record