The Paley--Zygmund inequality

For a nonnegative extended-real random variable Z with finite mean on a probability space and a level rho, the mass above rho * E Z is bounded below by the second-moment ratio,

(1 - rho) ^ 2 * (E Z) ^ 2 ≤ E (Z ^ 2) * mu {rho * E Z ≤ Z}.

The subtraction is the truncated one of ℝ≥0∞, so a level rho ≥ 1 leaves the trivial bound and needs no separate hypothesis. The primary form (MeasureTheory.lintegral_sq_mul_measure_ge_le) is division-free, so it needs neither positivity nor finiteness of the second moment; the divided form (MeasureTheory.le_measure_ge_of_lintegral_sq_ne_top) is the familiar (1 - rho) ^ 2 (E Z) ^ 2 / E (Z ^ 2) ≤ mu {rho * E Z ≤ Z}, whose finite-mean hypothesis is supplied by the second moment through the Cauchy--Schwarz inequality (MeasureTheory.lintegral_le_rpow_lintegral_sq).

Everything is stated for ℝ≥0∞-valued functions and carries no integrability side condition.

theorem MeasureTheory.setLIntegral_le_rpow_lintegral_sq_mul_rpow {Omega : Type u_1} [MeasurableSpace Omega] (mu : Measure Omega) {Z : Omega → ENNReal} (hZ : AEMeasurable Z mu) {A : Set Omega} (hA : MeasurableSet A) : ∫⁻ (omega : Omega) in A, Z omega ∂mu ≤ (∫⁻ (omega : Omega), Z omega ^ 2 ∂mu) ^ (1 / 2) * mu A ^ (1 / 2)

Cauchy--Schwarz on a measurable set: the integral of a nonnegative extended-real function over A is at most the square root of its second moment times the square root of the mass of A.

theorem MeasureTheory.lintegral_le_rpow_lintegral_sq {Omega : Type u_1} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] {Z : Omega → ENNReal} (hZ : AEMeasurable Z mu) : ∫⁻ (omega : Omega), Z omega ∂mu ≤ (∫⁻ (omega : Omega), Z omega ^ 2 ∂mu) ^ (1 / 2)

A finite second moment on a probability space forces a finite mean.

theorem MeasureTheory.lintegral_sq_mul_measure_ge_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] {Z : Omega → ENNReal} (hZ : Measurable Z) (hfin : ∫⁻ (omega : Omega), Z omega ∂mu ≠ ⊤) (rho : NNReal) : (1 - ↑rho) ^ 2 * (∫⁻ (omega : Omega), Z omega ∂mu) ^ 2 ≤ (∫⁻ (omega : Omega), Z omega ^ 2 ∂mu) * mu {omega : Omega | ↑rho * ∫⁻ (omega : Omega), Z omega ∂mu ≤ Z omega}

The Paley--Zygmund inequality, in division-free form: on a probability space the mass of the event {rho * E Z ≤ Z} obeys (1 - rho) ^ 2 * (E Z) ^ 2 ≤ E (Z ^ 2) * mu {rho * E Z ≤ Z}. The subtraction is the truncated one of ℝ≥0∞, so a level rho ≥ 1 gives the trivial bound 0 ≤ ….

theorem MeasureTheory.le_measure_ge_of_lintegral_sq_ne_top {Omega : Type u_1} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] {Z : Omega → ENNReal} (hZ : Measurable Z) (hsq : ∫⁻ (omega : Omega), Z omega ^ 2 ∂mu ≠ ⊤) (rho : NNReal) : (1 - ↑rho) ^ 2 * (∫⁻ (omega : Omega), Z omega ∂mu) ^ 2 / ∫⁻ (omega : Omega), Z omega ^ 2 ∂mu ≤ mu {omega : Omega | ↑rho * ∫⁻ (omega : Omega), Z omega ∂mu ≤ Z omega}

The Paley--Zygmund inequality, in divided form. The finite-mean hypothesis of the division-free version is supplied by the finite second moment.