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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 709 to 714 of 2,569 results.
DE₄_qexp
Mathematical 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
Mathematical 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.
debate_eq_transposed
Mathematical statement
The transposed formulation of debate is the same
Source project: debate
Person-level attribution pending.
decrypt_usesAtMostOneQuery
Mathematical statement
T-transform decryption makes at most one hash-oracle query under unit-cost instrumentation.
Source project: VCVio
Person-level attribution pending.
DeGiorgi.abs_ballAverage_sub_sixBallAverage_le
Mathematical statement
The average shift estimate: |(u)_B - (u)_{6B}| ≤ 6^d * M.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_sub_const_bmo_le_two
Mathematical statement
The absolute value function |u - c| has BMO seminorm at most 2M whenever u has BMO seminorm at most M. Uses the reverse triangle inequality ||a| - |b|| ≤ |a - b|.
Source project: DeGiorgi
Person-level attribution pending.