feat(Probability): add Paley-Zygmund inequality by Gracie-z · Pull Request #40835 · leanprover-community/mathlib4

Gracie-z · 2026-06-20T04:34:13Z

Add the Paley-Zygmund inequality: for a nonneg random variable Z with finite variance and 0 ≤ θ ≤ 1,
(1-θ)² E[Z]² ≤ E[Z²] · P(Z > θ E[Z]).

The proof uses Jensen's inequality applied to x² on the set {Z > θ E[Z]}.

AI disclosure: I used Claude Code as a learning aid while writing this proof. It helped me find the right Mathlib lemma names and understand tactic syntax, but I wrote every line of code myself.

github-actions · 2026-06-20T04:34:24Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-06-20T04:35:35Z

PR summary ac7311c75b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Probability.PaleyZygmund` (new file)	2710

Declarations diff (regex)

+ paley_zygmund

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ac7311c).

+1 new declarations
−0 removed declarations

+ProbabilityTheory.paley_zygmund

No changes to strong technical debt.

No changes to weak technical debt.

Current commit ac7311c75b
Reference commit c9ba3100f3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

github-actions · 2026-06-20T04:35:37Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

CoolRmal

The comments below are mostly about code styles and you can learn about them over here https://leanprover-community.github.io/contribute/style.html. However, some of them are probably not necessary as I have some suggestions about the overall design that can lead to some large changes for your PR.

There's nothing special about 2 here. You should prove it for any p : ℝ≥0∞ such that 1 <p<∞. It is possible that some version of this inequality is true for the endpoints 1 and ∞, but I didn't check them now.
I think it is better to first prove the following version:
(∫ ω, Z ω ∂μ - a) ^ 2 ≤ (∫ ω, Z ω ^ 2 ∂μ) * μ.real {ω | a < Z ω} for any 0≤a≤∫ ω, Z ω ∂μ (for simplicity I used 2 here but you should use a general p as I mentioned above). And then you can prove the inequality you want as a special case of a = θ * ∫ ω, Z ω ∂μ. You can argue that in some sense they are equivalent, but I think this version is more widely applicable.
In fact, the theorem above is not really optimal. You can even prove that (∫ ω, Z ω ∂μ - a) ^ 2 ≤ (∫ ω, Z ω ^ 2 ∂μ) * μ.real {ω | a < Z ω} is true for any (μ.real {ω | 0 < Z ω})⁻¹ * 0≤a≤∫ ω, Z ω ∂μ. This gives the following better inequality that you can find on wikipedia:

Let's go even further. Is it really necessary to assume that Z is real valued? The main theorems you used include setIntegral_mono_on₀ and ConvexOn.map_set_average_le, and these should work for any random variables taking values in a space E such that the following holds:
[NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [HasSolidNorm]. Of course, you also need to adapt the theorem that you want to prove a little bit:

‖∫ ω, Z ω ∂μ - a‖ ^ 2 ≤ ∫ ω, ‖Z ω‖ ^ 2 ∂μ * μ.real {ω | a < Z ω} is true for any 0≤a≤ (μ.real {ω | 0 < Z ω})⁻¹ • ∫ ω, Z ω ∂μ

You can then include the real version as an easy corollary of this theorem

CoolRmal · 2026-06-20T06:18:04Z

+public import Mathlib.Probability.Moments.Variance
+public import Mathlib.MeasureTheory.Integral.Bochner.Set
+public import Mathlib.Analysis.Convex.Integral
+public import Mathlib.Analysis.Convex.Mul


Suggested change

public import Mathlib.Probability.Moments.Variance

public import Mathlib.MeasureTheory.Integral.Bochner.Set

public import Mathlib.Analysis.Convex.Integral

public import Mathlib.Analysis.Convex.Mul

public import Mathlib.MeasureTheory.Function.L2Space

import Mathlib.Analysis.Convex.Integral

This is enough. Adding #min_imports at the bottom of a file can help you figure out the minimum import needed. You can check out this thread to learn when should one use public import: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/module.20system.20questions

CoolRmal · 2026-06-20T06:23:26Z

+  {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : (1 - θ) ^ 2 * (∫ ω, Z ω ∂μ) ^ 2 ≤ (∫ ω, Z ω ^ 2 ∂μ)
+  * (μ {ω | θ * ∫ ω', Z ω' ∂μ < Z ω}).toReal := by


Suggested change

{θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : (1 - θ) ^ 2 * (∫ ω, Z ω ∂μ) ^ 2 ≤ (∫ ω, Z ω ^ 2 ∂μ)

* (μ {ω | θ * ∫ ω', Z ω' ∂μ < Z ω}).toReal := by

{θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) :

(1 - θ) ^ 2 * (∫ ω, Z ω ∂μ) ^ 2 ≤

(∫ ω, Z ω ^ 2 ∂μ) * μ.real {ω | θ * ∫ ω, Z ω ∂μ < Z ω} := by

Need an extra indent here, and I think it is better to be consistent with the variable used inside the integral. Measure.real is more commonly used in the library. Always put an infix operator before the line break.

CoolRmal · 2026-06-20T06:30:39Z

+          apply mul_le_of_le_one_left (mul_nonneg hθ0 hZ_int_nn)
+            measureReal_le_one


Suggested change

apply mul_le_of_le_one_left (mul_nonneg hθ0 hZ_int_nn)

measureReal_le_one

apply mul_le_of_le_one_left (mul_nonneg hθ0 hZ_int_nn) measureReal_le_one

No need to have a line break as it is short enough.

CoolRmal · 2026-06-20T06:31:28Z

+  have h_cs: (∫ ω in S, Z ω ∂μ) ^ 2 ≤
+    (∫ ω, Z ω ^ 2 ∂μ ) * (μ S).toReal:= by
+    by_cases hS : μ S = 0
+    · simp [Measure.restrict_eq_zero.mpr, hS]
+    · have h_jensen := ConvexOn.map_set_average_le
+        even_two.convexOn_pow
+        (continuous_pow 2).continuousOn
+        isClosed_univ
+        hS
+        (measure_ne_top μ S)
+        (by simp)
+        hZ_int.integrableOn
+        hZ2.integrable_sq.integrableOn


Similarly there are two many unnecessary line breaks here.

CoolRmal · 2026-06-20T06:32:58Z

+    _ ≤ (∫ ω in S, Z ω ∂μ) ^ 2 := by
+      apply pow_le_pow_left₀ (mul_nonneg (sub_nonneg.mpr hθ1) hZ_int_nn) h_lower


Suggested change

_ ≤ (∫ ω in S, Z ω ∂μ) ^ 2 := by

apply pow_le_pow_left₀ (mul_nonneg (sub_nonneg.mpr hθ1) hZ_int_nn) h_lower

_ ≤ (∫ ω in S, Z ω ∂μ) ^ 2 :=

pow_le_pow_left₀ (mul_nonneg (sub_nonneg.mpr hθ1) hZ_int_nn) h_lower 2

by exact or by apply is not prefered if you can formalize with a single proof term.

CoolRmal · 2026-06-20T06:39:33Z

+      rw [setAverage_eq, setAverage_eq, smul_eq_mul, smul_eq_mul, mul_pow, sq ((μ.real S)⁻¹),
+      mul_assoc, mul_le_mul_iff_of_pos_left (inv_pos.mpr hμS_pos), mul_comm,
+      ← div_eq_mul_inv, div_le_iff₀ hμS_pos, measureReal_def] at h_jensen


Suggested change

rw [setAverage_eq, setAverage_eq, smul_eq_mul, smul_eq_mul, mul_pow, sq ((μ.real S)⁻¹),

mul_assoc, mul_le_mul_iff_of_pos_left (inv_pos.mpr hμS_pos), mul_comm,

← div_eq_mul_inv, div_le_iff₀ hμS_pos, measureReal_def] at h_jensen

rw [setAverage_eq, setAverage_eq, smul_eq_mul, smul_eq_mul, mul_pow, sq ((μ.real S)⁻¹),

mul_assoc, mul_le_mul_iff_of_pos_left (inv_pos.mpr hμS_pos), mul_comm,

← div_eq_mul_inv, div_le_iff₀ hμS_pos, measureReal_def] at h_jensen

CoolRmal · 2026-06-20T06:41:07Z

+          mul_le_mul_of_nonneg_right
+            (setIntegral_le_integral hZ2.integrable_sq (ae_of_all μ (fun x => sq_nonneg (Z x))))
+            ENNReal.toReal_nonneg


Suggested change

mul_le_mul_of_nonneg_right

(setIntegral_le_integral hZ2.integrable_sq (ae_of_all μ (fun x => sq_nonneg (Z x))))

ENNReal.toReal_nonneg

gcongr ?_ * ?_

exact setIntegral_le_integral hZ2.integrable_sq (ae_of_all μ (fun x => sq_nonneg (Z x)))

gcongr saves you effort for find theorems like mul_le_mul_of_nonneg_right

SnirBroshi · 2026-06-20T11:38:50Z

Hello, can you disclose if and how you used LLMs in the creation of this PR, per the contribution guidelines?

Gracie-z · 2026-06-20T15:33:20Z

Hello, can you disclose if and how you used LLMs in the creation of this PR, per the contribution guidelines?

Hi, I just update my PR description. Thanks for the reminder!

Gracie and others added 7 commits June 19, 2026 08:49

add Paley-Zygmund inequality statement, complete initial setup

454daa4

commit after pulling

4725224

Merge branch 'master' into Paley-Zygmund

e240c0f

build proof structure

aaea260

finish formalization

1bca104

take out the checks

06136bc

add PaleyZygmund inequality to Mathlib.lean

ac7311c

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 20, 2026

github-actions Bot added the t-measure-probability Measure theory / Probability theory label Jun 20, 2026

Gracie-z changed the title ~~feat(Probability): Paley-Zygmund inequality~~ feat(Probability): add Paley-Zygmund inequality Jun 20, 2026

CoolRmal reviewed Jun 20, 2026

View reviewed changes

		{θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : (1 - θ) ^ 2 * (∫ ω, Z ω ∂μ) ^ 2 ≤ (∫ ω, Z ω ^ 2 ∂μ)
		* (μ {ω \| θ * ∫ ω', Z ω' ∂μ < Z ω}).toReal := by

		apply mul_le_of_le_one_left (mul_nonneg hθ0 hZ_int_nn)
		measureReal_le_one

		_ ≤ (∫ ω in S, Z ω ∂μ) ^ 2 := by
		apply pow_le_pow_left₀ (mul_nonneg (sub_nonneg.mpr hθ1) hZ_int_nn) h_lower

Conversation

Gracie-z commented Jun 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 20, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Jun 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ac7311c75b

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

github-actions Bot commented Jun 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

CoolRmal left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

CoolRmal Jun 20, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi commented Jun 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Gracie-z commented Jun 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Gracie-z commented Jun 20, 2026 •

edited

Loading

github-actions Bot commented Jun 20, 2026 •

edited

Loading

github-actions Bot commented Jun 20, 2026 •

edited

Loading

CoolRmal left a comment •

edited

Loading

SnirBroshi commented Jun 20, 2026 •

edited

Loading

Gracie-z commented Jun 20, 2026 •

edited

Loading