The Marcinkiewicz-Zygmund inequality

This file proves the Marcinkiewicz-Zygmund inequality.

theorem Real.marcinkiewicz_zygmund' {ι : Type u_1} {A : Finset ι} {n : ℕ} (m : ℕ) (f : ι → ℝ) (hf : ∀ (i : Fin n), ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, f (a i) = 0) : ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, (∑ i : Fin n, f (a i)) ^ (2 * m) ≤ (4 * ↑m) ^ m * ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, (∑ i : Fin n, f (a i) ^ 2) ^ m

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly better constant than Real.marcinkiewicz_zygmund.

theorem Real.marcinkiewicz_zygmund {ι : Type u_1} {A : Finset ι} {m n : ℕ} (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ (i : Fin n), ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, f (a i) = 0) : ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, (∑ i : Fin n, f (a i)) ^ (2 * m) ≤ (4 * ↑m) ^ m * ↑n ^ (m - 1) * ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, ∑ i : Fin n, f (a i) ^ (2 * m)

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.

theorem RCLike.marcinkiewicz_zygmund {ι : Type u_1} {A : Finset ι} {m n : ℕ} {𝕜 : Type u_2} [RCLike 𝕜] (hm : m ≠ 0) (f : ι → 𝕜) (hf : ∀ (i : Fin n), ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, f (a i) = 0) : ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, ‖∑ i : Fin n, f (a i)‖ ^ (2 * m) ≤ (8 * ↑m) ^ m * ↑n ^ (m - 1) * ∑ a ∈ Fintype.piFinset fun (x : Fin n) => A, ∑ i : Fin n, ‖f (a i)‖ ^ (2 * m)

The Marcinkiewicz-Zygmund inequality for real- or complex-valued functions.