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 filtersD_real_of_real
Plain-language statement
If F is real on the imaginary axis and MDifferentiable, then D F is also real on the imaginary axis.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
D_slash
Plain-language statement
The derivative anomaly: how D interacts with the slash action. This is the key computation for proving Serre derivative equivariance.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
D_tendsto_zero_of_isBoundedAtImInfty
Plain-language statement
The D-derivative of a bounded holomorphic function tends to zero at infinity. For z with im(z) = y, a Cauchy estimate on a ball of radius y/2 gives ‖D f z‖ ≤ M / (π · y), which tends to zero as y → ∞.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_imag_axis_re_pos
Plain-language statement
The real part of (D E₄)(it) is positive for t > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_qexp
Plain-language statement
D E₄ q-expansion via termwise differentiation. D E₄ = 240 * ∑ n * σ₃(n) * qⁿ from differentiating E₄ = 1 + 240 * ∑ σ₃(n) * qⁿ.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
DE₄_term_re_pos
Plain-language statement
Each term n*σ₃(n)*exp(-2πnt) in D E₄ q-expansion has positive real part on imaginary axis.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.