The Marcinkiewicz-Zygmund inequality

This file proves the Marcinkiewicz-Zygmund inequality.

The Marcinkiewicz-Zygmund inequality states that, if X₁, ... Xₐ ∈ L^p are independent random variables of mean zero valued in some inner product space, then the L^p-norm of X₁ + ... + Xₐ is at most Cₚ times the L^(p/2)-norm of |X₁|² + ... + |Xₐ|², where Cₚ is a constant depending on p alone.

Notation

Throughout this file, A ^^ n denotes A × ... × A (with n factors). Formally, this is Fintype.piFinset fun _ : Fin n ↦ A.

TODO

We currently only prove the inequality for p = 2 * m an even natural number. The general p case can be obtained from this specific one by nesting of Lp norms.

noncomputable def marcinkiewiczZygmundSymmConst (p : NNReal) : ℝ

The constant appearing in the Marcinkiewicz-Zygmund inequality for symmetric random variables.

Equations

• marcinkiewiczZygmundSymmConst p = (↑p / 2) ^ (↑p / 2)

theorem marcinkiewicz_zygmund_symmetric {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {A : Finset ι} {m : ℕ} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [mE : MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : ι → Ω → E} (iIndepFun_X : ProbabilityTheory.iIndepFun X μ) (identDistrib_neg_X : ∀ (i : ι), ProbabilityTheory.IdentDistrib (X i) (-X i) μ μ) (memLp_X : ∀ i ∈ A, MeasureTheory.MemLp (X i) (2 * ↑m) μ) : ∫ (ω : Ω), ‖∑ i ∈ A, X i ω‖ ^ (2 * m) ∂μ ≤ marcinkiewiczZygmundSymmConst (2 * ↑m) * ∫ (ω : Ω), (∑ i ∈ A, ‖X i ω‖ ^ 2) ^ m ∂μ

The Marcinkiewicz-Zygmund inequality for symmetric random variables, with a slightly better constant than marcinkiewicz_zygmund.

noncomputable def marcinkiewiczZygmundConst (p : NNReal) : ℝ

The constant appearing in the Marcinkiewicz-Zygmund inequality for random variables with zero mean.

Equations

• marcinkiewiczZygmundConst p = 2 ^ (↑p / 2) * marcinkiewiczZygmundSymmConst p

theorem marcinkiewicz_zygmund {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {A : Finset ι} {m : ℕ} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [mE : MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : ι → Ω → E} (iIndepFun_X : ProbabilityTheory.iIndepFun X μ) (integral_X : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0) (memLp_X : ∀ i ∈ A, MeasureTheory.MemLp (X i) (2 * ↑m) μ) : ∫ (ω : Ω), ‖∑ i ∈ A, X i ω‖ ^ (2 * m) ∂μ ≤ marcinkiewiczZygmundConst (2 * ↑m) * ∫ (ω : Ω), (∑ i ∈ A, ‖X i ω‖ ^ 2) ^ m ∂μ

The Marcinkiewicz-Zygmund inequality for random variables with zero mean.

For symmetric random variables, marcinkiewicz_zygmund provides a slightly better constant.