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 filtersΔ_fun_eq_Δ
Plain-language statement
The discriminant Δ_fun = 1728⁻¹(E₄³ - E₆²) equals the standard discriminant Δ.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Θ₂_imag_axis_re_pos
Plain-language statement
Θ₂(It) has positive real part for t > 0. Proof: Each term Θ₂_term n (It) = exp(-π(n+1/2)²t) is a positive real. The sum of positive reals is positive.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Θ₂_term_imag_axis_re
Plain-language statement
Each term Θ₂_term n (I*t) has positive real part equal to exp(-π(n+1/2)²t) for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
Θ₄_term_imag_axis_real
Plain-language statement
Each term Θ₄_term n (I*t) has zero imaginary part for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
φ₀_S_transform
Plain-language statement
The S-transformation formula for φ₀: φ₀(-1/z) = φ₀(z) - (12i/π)(1/z)φ₋₂(z) - (36/π²)(1/z²)φ₋₄(z) This is Blueprint Lemma 7.2.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.