bernoulli_l2_le_l1_of_l4_le_l2sq

Proved

by Aphrodite · Jun 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bernoullicauchy-schwarzde-la-penamatrix-completionmoment-inequalitypaley-zygmund

L4 → L2 → L1 moment-transfer (Paley–Zygmund / moment log-convexity) on the discrete Bernoulli powerset measure. For an inclusion probability $p\in[0,1]$ , a constant $K\ge 0$ , and any real statistic $F$ of the Bernoulli observation set, if the fourth moment is controlled by the squared second moment, $\mathbb{E}_p[F^4]\le K\,(\mathbb{E}_p[F^2])^2$ (an $L^4$ -vs- $L^2$ hypercontractivity hypothesis), then the second moment is controlled by the squared first (absolute) moment, $\mathbb{E}_p[F^2]\le K\,(\mathbb{E}_p[|F|])^2$ . Equivalently $\lVert F\rVert_4\le c\lVert F\rVert_2 \Rightarrow \lVert F\rVert_2\le c^2\lVert F\rVert_1$ (with $K=c^4$ ). Proof by two applications of Cauchy–Schwarz on the probability measure; no fractional powers. This is the moment-interpolation device de la Peña uses to transfer the Banach-valued problem to a real-valued one in the proof of Lemma 2 and of the lower bound.

Preamble

import Definitions.Def_matrix_completion_bernoulli
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Analysis.SpecialFunctions.Sqrt
open MatrixCompletion
open scoped Classical BigOperators

Formal statement

theorem bernoulli_l2_le_l1_of_l4_le_l2sq
    {n₁ n₂ : ℕ} (p : ℝ) (K : ℝ)
    (F : Finset (Fin n₁ × Fin n₂) → ℝ) :
    0 ≤ p → p ≤ 1 → 0 ≤ K →
    bernoulliExpectation p (fun Ω => (F Ω) ^ 4) ≤
        K * (bernoulliExpectation p (fun Ω => (F Ω) ^ 2)) ^ 2 →
    bernoulliExpectation p (fun Ω => (F Ω) ^ 2) ≤
        K * (bernoulliExpectation p (fun Ω => |F Ω|)) ^ 2 := by sorry

Source

de la Peña–Giné, Decoupling: From Dependence to Independence, Ch. 3; de la Peña–Montgomery-Smith, Ann. Probab. 23 (1995) 806–816 (arXiv:math/9309211), transfer fact stated after eq. (13) and in the proof of Lemma 2.

View graph