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.