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 199 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

199 results

Clear filters
Project-declaredLean 4.32.0

S truncation

S_truncation

Plain-language statement

Let 1<q21<q\le2, let qq' be its Hölder conjugate, and suppose the linearized nontangential operators have the required uniform L2L^2 bound. For bounded measurable F,GF,G and measurable ff with f(x)1F(x)\lVert f(x)\rVert\le\mathbf 1_F(x), the supremum over all truncated scale intervals Bs1s2B-B\le s_1\le s_2\le B satisfies

G+sups1s2Ts1,s2f(x)dxC(a,q)μ(G)1/qμ(F)1/q.\int_G^+\sup_{s_1\le s_2}\lVert T_{s_1,s_2}f(x)\rVert\,dx\le C(a,q)\,\mu(G)^{1/q'}\mu(F)^{1/q}.

harmonic analysisFourier analysismeasure theory

Source project: Carleson formalization

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Serre D is Bounded At Im Infty of bounded

serre_D_isBoundedAtImInfty_of_bounded

Plain-language statement

The Serre derivative of a bounded holomorphic function is bounded at infinity. serre_D k f = D f - (k/12)·E₂·f. Both terms are bounded: - D f is bounded by D_isBoundedAtImInfty_of_bounded - (k/12)·E₂·f is bounded since E₂ and f are bounded

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Serre D slash equivariant

serre_D_slash_equivariant

Plain-language statement

Serre derivative is equivariant under the slash action. More precisely, if F is invariant under the slash action of weight k, then serre_D k F is invariant under the slash action of weight k + 2.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Serre D tendsto of tendsto

serre_D_tendsto_of_tendsto

Project documentation

General limit: if f → c at i∞ and f is holomorphic and bounded, then serre_D k f → -k*c/12. This is the continuous mapping theorem applied to serre_D k f = D f - (k/12) * E₂ * f: - D f → 0 (Cauchy estimate from boundedness) - E₂ → 1 - f → c Therefore serre_D k f → 0 - (k/12) * 1 * c = -k*c/12.

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Serre DE₂ slash invariant

serre_DE₂_slash_invariant

Plain-language statement

The Serre derivative of E₂ is weight-4 slash-invariant. This requires explicit computation since E₂ is not modular. Proof strategy: Write serre_D 1 E₂ = serre_D 2 E₂ + (1/12) E₂². Then: - (serre_D 2 E₂) ∣[4] γ = serre_D 2 (E₂ ∣[2] γ) by serre_D_slash_equivariant - E₂ ∣[2] γ = E₂ - α D₂ γ where α = 1/(2ζ(2)) = 3/π² - (E₂²) ∣[4] γ = (E₂ ∣[2] γ)² After e...

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record