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 35 research declarations. Search 10,000 more complete Mathlib declarations.
35 results
Clear filtersderiv_moebius
Plain-language statement
Derivative of the Möbius transformation: d/dz[(az+b)/(cz+d)] = 1/(cz+d)². Uses det(γ) = 1: a(cz+d) - c(az+b) = ad - bc = 1.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
deriv_resToImagAxis_eq
Plain-language statement
Chain rule for restriction to imaginary axis: d/dt F(it) = -2π * (D F)(it). This connects the real derivative along the imaginary axis to the normalized derivative D. The key computation is: - The imaginary axis is parametrized by g(t) = I * t - By chain rule: d/dt F(it) = (dF/dz)(it) · (d/dt)(it) = F'(it) · I - Since D = (2πi)⁻¹ · d/dz, we have F' = 2π...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DifferentiableAt_MDifferentiableAt
Plain-language statement
The converse direction: DifferentiableAt on ℂ implies MDifferentiableAt on ℍ.
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₄_eq_H_sum_sq
Plain-language statement
E₄.toFun = H₂² + H₂H₄ + H₄². Both are weight-4 level-1 modular forms tending to 1 at ∞, so their difference is a weight-4 cusp form, hence zero.
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.