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 filtersDifferentiableAt_MDifferentiableAt
Plain-language statement
The converse direction: DifferentiableAt on ℂ implies MDifferentiableAt on ℍ.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E_even_imag_axis_real
Project documentation
E_k(it) is real for all t > 0 when k is even and k ≥ 4. This is the generalized theorem from which E₄_imag_axis_real and E₆_imag_axis_real follow.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_holo'
Plain-language statement
TODO: Move this to E2.lean.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_imag_axis_real
Plain-language statement
E₂(it) is real for all t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_isBoundedAtImInfty
Plain-language statement
E₂ is bounded at infinity. Uses E₂_eq: E₂(z) = 1 - 24·Σₙ₌₁ n·qⁿ/(1-qⁿ) where q = exp(2πiz). For im(z) ≥ 1, |q| ≤ exp(-2π), so by norm_tsum_logDeriv_expo_le, |E₂| ≤ 1 + 24·exp(-2π)/(1-exp(-2π))³.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
E₂_mul_E₄_sub_E₆
Plain-language statement
The q-expansion identity E₂E₄ - E₆ = 720·Σn·σ₃(n)·qⁿ. This follows from Ramanujan's formula: E₂E₄ - E₆ = 3·D(E₄), combined with D(E₄) = 240·Σn·σ₃(n)·qⁿ (since D multiplies q-coefficients by n).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.