Rudin ineq
rudin_ineq
Plain-language statement
Rudin's inequality, usual form.
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersrudin_ineq
Plain-language statement
Rudin's inequality, usual form.
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
S_truncation
Plain-language statement
Let , let be its Hölder conjugate, and suppose the linearized nontangential operators have the required uniform bound. For bounded measurable and measurable with , the supremum over all truncated scale intervals satisfies
Source project: Carleson formalization
Person-level attribution pending.
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
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
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.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
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.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
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...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.