Source-pinned research

Research proof index

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.

1 topic

35 results

Clear filters
Project-declaredLean 4.31.0

Anti Der Pos

antiDerPos

Plain-language statement

If FF is a modular form where F(it)F(it) is positive for sufficiently large tt (i.e. constant term is positive) and the derivative is positive, then FF is also positive.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Anti Serre Der Pos

antiSerreDerPos

Plain-language statement

Let F:HCF : \mathbb{H} \to \mathbb{C} be a holomorphic function where F(it)F(it) is real for all t>0t > 0. Assume that Serre derivative kF\partial_k F is positive on the imaginary axis. If F(it)F(it) is positive for sufficiently large tt, then F(it)F(it) is positive for all t>0t > 0.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

D add

D_add

Plain-language statement

Basic properties of derivatives: linearity, Leibniz rule, etc.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

D is Bounded At Im Infty of bounded

D_isBoundedAtImInfty_of_bounded

Plain-language statement

The D-derivative is bounded at infinity for bounded holomorphic functions. For y large (y ≥ 2·max(A,0) + 1), we use a ball of radius z.im/2 around z. The ball lies in the upper half plane, f is bounded by M on it, and norm_D_le_of_sphere_bound gives ‖D f z‖ ≤ M/(π·z.im) ≤ M/π.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

D qexp term

D_qexp_term

Plain-language statement

Lemma 6.45 (Blueprint): The normalized derivative DD acts as qddqq \frac{d}{dq} on qq-series. For a single q-power term: D(a·qⁿ) = n·a·qⁿ where q = exp(2πiz) and n ∈ ℤ. The key calculation: - d/dz(exp(2πinz)) = 2πin·exp(2πinz) - D(exp(2πinz)) = (2πi)⁻¹·(2πin·exp(2πinz)) = n·exp(2πinz)

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record