The mean squared distance between two independent copies and nonzero-variance bounds

Let f be a square-integrable function, with values in a real Hilbert space, on a finite measure space (α, μ). Then

∫∫ ‖f x - f y‖² dμ(x) dμ(y) = 2 (μ(α) ∫ ‖f‖² dμ - ‖∫ f dμ‖²).

For a probability measure the right-hand side is twice the variance ∫ ‖f‖² dμ - ‖∫ f dμ‖² of f, the trace of its covariance: the mean squared distance between two independent samples of f is twice its variance. Expanding ‖u - v‖² = ‖u‖² + ‖v‖² - 2 ⟪u, v⟫, the cross term integrates to ‖∫ f dμ‖² because the two coordinates are integrated separately.

This identity is what turns the strong-convexity remainder of an interaction energy along a transport plan, an integral over pairs of transported pairs, into the variance of the displacement.

The file also records the elementary bound of the mean of a real function by the square root of its second moment (the nonnegativity of its variance), together with two consequences of nonzero variance Var[X; μ] ≠ 0: strict positivity of the expectation of an ℝ≥0-valued random variable on a finite measure space, and nondegeneracy μ {ω | X ω = 0} < 1 of a real-valued random variable on a probability space.

Main statements

• MeasureTheory.MemLp.integrable_norm_sub_sq_prod: for f ∈ L²(μ) and a finite measure μ, the function (x, y) ↦ ‖f x - f y‖² is integrable for μ ⊗ μ.
• TauCeti.integral_norm_sub_sq_prod: the identity above.
• MeasureTheory.integral_le_sqrt_integral_sq: on a probability space, the mean of a real square-integrable function is at most the square root of its second moment, which is the nonnegativity of its variance.
• MeasureTheory.MeasurePreserving.evariance_fun_comp: the variance is invariant under composition with a measure-preserving measurable embedding.
• ProbabilityTheory.tendsto_variance_of_tendsto_eLpNorm_sub: variance is continuous under L² convergence on a finite measure space.
• TauCeti.Probability.evariance_integral_prod_le and TauCeti.Probability.evariance_prod_le: product-variance bounds for averages and products.
• TauCeti.Probability.variance_weighted_coordinate_sum and TauCeti.Probability.measure_weighted_coordinate_sum_sub_mean_ge: variance and Chebyshev bounds for weighted sums of pairwise independent variables.
• TauCeti.integral_coe_pos_of_variance_ne_zero: on a finite measure space, an ℝ≥0-valued random variable with nonzero variance has strictly positive expectation.
• TauCeti.measure_setOf_eq_zero_lt_one_of_variance_ne_zero: on a probability space, a real-valued random variable with nonzero variance satisfies μ {ω | X ω = 0} < 1.

theorem ProbabilityTheory.tendsto_variance_of_tendsto_eLpNorm_sub {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ} {g : ι → α → ℝ} {l : Filter ι} (hf : MeasureTheory.MemLp f 2 μ) (hg : ∀ (i : ι), MeasureTheory.MemLp (g i) 2 μ) (ht : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (g i - f) 2 μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => variance (g i) μ) l (nhds (variance f μ))

The variance is continuous under L² convergence on a finite measure space.

theorem MeasureTheory.MemLp.integrable_norm_sub_sq_prod {α : Type u_1} {E : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [IsFiniteMeasure μ] {f : α → E} (hf : MemLp f 2 μ) : Integrable (fun (z : α × α) => ‖f z.1 - f z.2‖ ^ 2) (μ.prod μ)

For a square-integrable function f on a finite measure space, (x, y) ↦ ‖f x - f y‖² is integrable for the product of the measure with itself.

theorem MeasureTheory.integral_le_sqrt_integral_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {g : Ω → ℝ} (hg : MemLp g 2 μ) : ∫ (x : Ω), g x ∂μ ≤ √(∫ (x : Ω), g x ^ 2 ∂μ)

On a probability space, the mean of a square-integrable function is at most the square root of its second moment.

theorem TauCeti.integral_norm_sub_sq_prod {α : Type u_1} {E : Type u_2} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : ∫ (z : α × α), ‖f z.1 - f z.2‖ ^ 2 ∂μ.prod μ = 2 * (μ.real Set.univ * ∫ (x : α), ‖f x‖ ^ 2 ∂μ - ‖∫ (x : α), f x ∂μ‖ ^ 2)

The mean squared distance between two independent copies. For a square-integrable function f with values in a real Hilbert space and a finite measure μ, ∫∫ ‖f x - f y‖² dμ(x) dμ(y) = 2 (μ(α) ∫ ‖f‖² dμ - ‖∫ f dμ‖²). For a probability measure this is twice the variance of f.

theorem TauCeti.integral_coe_pos_of_variance_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → NNReal} (hX : AEMeasurable X μ) (hvar : ProbabilityTheory.variance (fun (ω : Ω) => ↑(X ω)) μ ≠ 0) : 0 < ∫ (ω : Ω), ↑(X ω) ∂μ

A nonnegative random variable on a finite measure space with nonzero variance has strictly positive real expectation.

theorem TauCeti.measure_setOf_eq_zero_lt_one_of_variance_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hvar : ProbabilityTheory.variance X μ ≠ 0) : μ {ω : Ω | X ω = 0} < 1

On a probability space, a real-valued random variable with nonzero variance is not almost surely zero.

theorem MeasureTheory.MeasurePreserving.evariance_fun_comp {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : Measure Ω} {ν : Measure Ω'} {e : Ω → Ω'} (he : MeasurePreserving e μ ν) (hem : MeasurableEmbedding e) (f : Ω' → ℝ) : ProbabilityTheory.evariance (fun (x : Ω) => f (e x)) μ = ProbabilityTheory.evariance f ν

The variance is invariant under composition with a measure-preserving measurable embedding.

theorem TauCeti.Probability.variance_weighted_coordinate_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (a : ι → ℝ) (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 P) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) P) : ProbabilityTheory.variance (fun (ω : Ω) => ∑ i : ι, a i * X i ω) P = ∑ i : ι, a i ^ 2 * ProbabilityTheory.variance (X i) P

The variance of a weighted sum of pairwise independent square-integrable variables.

theorem TauCeti.Probability.measure_weighted_coordinate_sum_sub_mean_ge {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ι → Ω → ℝ} (a : ι → ℝ) (hX : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 P) (hindep : Pairwise fun (i j : ι) => ProbabilityTheory.IndepFun (X i) (X j) P) {ε : ℝ} (hε : 0 < ε) : P {ω : Ω | ε ≤ |∑ i : ι, a i * X i ω - ∫ (ω : Ω), ∑ i : ι, a i * X i ω ∂P|} ≤ ENNReal.ofReal ((∑ i : ι, a i ^ 2 * ProbabilityTheory.variance (X i) P) / ε ^ 2)

Chebyshev's bound for a weighted sum of pairwise independent variables.

theorem TauCeti.Probability.evariance_integral_prod_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure α} {π : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure π] {F : α × β → ℝ} (hint : MeasureTheory.Integrable F (ν.prod π)) : ProbabilityTheory.evariance (fun (a : α) => ∫ (w : β), F (a, w) ∂π) ν ≤ ∫⁻ (w : β), ProbabilityTheory.evariance (fun (a : α) => F (a, w)) ν ∂π

Jensen's inequality for the variance of an average: the variance of the average over the second coordinate is at most the average over the second coordinate of the variances in the first coordinate.

theorem TauCeti.Probability.evariance_prod_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure α} {π : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure π] {F : α × β → ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hL : MeasureTheory.MemLp F 2 (ν.prod π)) : ProbabilityTheory.evariance F (ν.prod π) ≤ ∫⁻ (a : α), ProbabilityTheory.evariance (fun (w : β) => F (a, w)) π ∂ν + ∫⁻ (w : β), ProbabilityTheory.evariance (fun (a : α) => F (a, w)) ν ∂π

The two-factor Efron--Stein inequality.

theorem TauCeti.Probability.measurable_evariance_update {ι : Type u_3} [DecidableEq ι] {α : ι → Type u_4} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) (i : ι) [MeasureTheory.SFinite (μ i)] {f : ((i : ι) → α i) → ℝ} (hf : Measurable f) : Measurable fun (x : (a : ι) → α a) => ProbabilityTheory.evariance (fun (y : α i) => f (Function.update x i y)) (μ i)

The variance of f in coordinate i, with the other coordinates frozen at x, is a measurable function of x.