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

1 topic

83 results

Clear filters
Project-declaredLean 4.32.0

D Lp Norm conjneg

MeasureTheory.dLpNorm_conjneg

Plain-language statement

The discrete normalized LpL^p norm is unchanged by conjugating a function and reflecting its argument: xf(x)p=fp\|x\mapsto\overline{f(-x)}\|_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

D Lp Norm pow

MeasureTheory.dLpNorm_pow

Plain-language statement

For nonzero natural exponents pp and qq, taking a pointwise qq-th power rescales the discrete normalized norm by fqp=fpqq\|f^q\|_p=\|f\|_{pq}^{q}.

additive combinatoricsarithmetic progressionsFourier analysis

Source project: Arithmetic Progressions Almost Periodicity

Person-level attribution pending.

View proof record
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