Chebyshev's integral inequality and empirical covariance [UPSTREAM]

Two real random variables that monovary have nonnegative covariance, and two that antivary have nonpositive covariance. On a finite measure the statement is (∫ X ∂μ) * ∫ Y ∂μ ≤ μ.real univ * ∫ X * Y ∂μ, the integral form of Chebyshev's sum inequality (MonovaryOn.sum_mul_sum_le_card_mul_sum); on a probability measure it reads 0 ≤ cov[X, Y; μ].

Under the uniform measure on a finite type the covariance is the sample covariance, the mean of the products less the product of the means, and it is positive exactly when the sum of products exceeds the product of the sums divided by the sample size.

Main declarations

• Monovary.integral_mul_integral_le_measureReal_univ_mul_integral, Antivary.measureReal_univ_mul_integral_le_integral_mul_integral: Chebyshev's integral inequality on a finite measure and its dual.
• Monovary.covariance_nonneg, Antivary.covariance_nonpos: the covariance forms.
• covariance_uniformOn_univ, covariance_uniformOn_univ_pos_iff: the sample covariance under the uniform measure on a finite type and the sign of its numerator.

Implementation notes

The proof integrates 0 ≤ (X ω - X ω') * (Y ω - Y ω'), pointwise nonnegative by Monovary.sub_mul_sub_nonneg, over the product measure μ.prod μ, where it expands to twice the covariance defect. The dual follows by negating X.

theorem Monovary.integral_mul_integral_le_measureReal_univ_mul_integral {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Integrable X μ) (hY : MeasureTheory.Integrable Y μ) (hXY : MeasureTheory.Integrable (X * Y) μ) (h : Monovary X Y) : (∫ (ω : Ω), X ω ∂μ) * ∫ (ω : Ω), Y ω ∂μ ≤ μ.real Set.univ * ∫ (ω : Ω), X ω * Y ω ∂μ

Chebyshev's integral inequality: when X and Y monovary, the product of their integrals is at most the total mass times the integral of their product.

theorem Antivary.measureReal_univ_mul_integral_le_integral_mul_integral {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.Integrable X μ) (hY : MeasureTheory.Integrable Y μ) (hXY : MeasureTheory.Integrable (X * Y) μ) (h : Antivary X Y) : μ.real Set.univ * ∫ (ω : Ω), X ω * Y ω ∂μ ≤ (∫ (ω : Ω), X ω ∂μ) * ∫ (ω : Ω), Y ω ∂μ

Chebyshev's integral inequality: when X and Y antivary, the product of their integrals is at least the total mass times the integral of their product.

theorem Monovary.covariance_nonneg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (h : Monovary X Y) : 0 ≤ ProbabilityTheory.covariance X Y μ

Random variables that monovary have nonnegative covariance.

theorem Antivary.covariance_nonpos {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (hY : MeasureTheory.MemLp Y 2 μ) (h : Antivary X Y) : ProbabilityTheory.covariance X Y μ ≤ 0

Random variables that antivary have nonpositive covariance.

theorem ProbabilityTheory.integral_uniformOn_univ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [MeasurableSingletonClass Ω] [Fintype Ω] (f : Ω → ℝ) : ∫ (ω : Ω), f ω ∂uniformOn Set.univ = (∑ ω : Ω, f ω) / ↑(Fintype.card Ω)

The integral under the uniform measure on a finite type is the sample mean.

theorem ProbabilityTheory.covariance_uniformOn_univ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] : covariance X Y (uniformOn Set.univ) = (∑ ω : Ω, X ω * Y ω) / ↑(Fintype.card Ω) - (∑ ω : Ω, X ω) / ↑(Fintype.card Ω) * ((∑ ω : Ω, Y ω) / ↑(Fintype.card Ω))

The covariance under the uniform measure on a finite type is the sample covariance.

theorem ProbabilityTheory.covariance_uniformOn_univ_pos_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) [MeasurableSingletonClass Ω] [Fintype Ω] [Nonempty Ω] : 0 < covariance X Y (uniformOn Set.univ) ↔ (∑ ω : Ω, X ω) * ∑ ω : Ω, Y ω < ↑(Fintype.card Ω) * ∑ ω : Ω, X ω * Y ω

The sample covariance is positive exactly when the product of the sums is less than the sample size times the sum of the products.