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

1 topic

38 results

Clear filters
Project-declaredLean 4.32.0

D Lp Norm translate

MeasureTheory.dLpNorm_translate

Plain-language statement

Translation preserves the discrete normalized LpL^p norm: for every group element aa, τafp=fp\|\tau_a f\|_{p}=\|f\|_{p}.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Pow inner nonneg

pow_inner_nonneg'

Project documentation

A positivity lemma for self-difference-convolutions. If f=ggf=g\mathbin{\circleddash}g and the nonnegative weight ν\nu has a factorization ν=hh\nu=h\mathbin{\circleddash}h, then every natural power of ff has nonnegative weighted inner product with ν\nu: fk,ν0\langle f^k,\nu\rangle\ge0 for every kNk\in\mathbb N.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Marcinkiewicz zygmund

Real.marcinkiewicz_zygmund

Plain-language statement

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly easier to bound constant than Real.marcinkiewicz_zygmund'. Note that RCLike.marcinkiewicz_zygmund is another version that works for both and at the expense of a slightly worse constant.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record