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 101 research declarations. Search 10,000 more complete Mathlib declarations.
101 results
Clear filtersF_functional_equation
Project documentation
Reduce a power of I * w via I ^ 4 = 1. -/ lemma I_mul_npow (w : ℂ) (n : ℕ) : (I * w) ^ n = I ^ (n % 4) * w ^ n := by rw [mul_pow, I_pow_eq_pow_mod] /- Functional equation of
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
F_functional_equation'
Plain-language statement
Functional equation of restricted to the imaginary axis.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
F_vanishing_order
Plain-language statement
The vanishing order of F at infinity is 2. Blueprint: F = 720² * q² * (1 + O(q)), so F / q² → 720² as im(z) → ∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
F₁_isBigO_exp_atImInfty
Plain-language statement
F₁ has exponential decay at infinity (it's essentially D E₄ which decays).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_add_f₄_eq_f₃
Plain-language statement
The error terms satisfy f₂ + f₄ = f₃ (from Jacobi identity)
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_eq_zero
Plain-language statement
From g = 0 and h = 0, deduce f₂ = 0. Proof: From g = 0 we get a relation between f₂ and f₄. Combined with h = 0, we show f₄² · (3 · H_sum_sq) = 0. Since H_sum_sq → 1 ≠ 0, we get f₄ = 0, then f₂ = 0 follows from h = f₂² = 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.