The quadratic Fenchel–Young inequality in mean

For a positive-semidefinite matrix A with pseudoinverse A⁺, the quadratic Fenchel–Young inequality ⟪u, y⟫ ≤ (⟪A y, y⟫ + ⟪A⁺ u, u⟫) / 2 holds for every y and every u in the range of A. This file takes it in mean, for a centred random vector u = X - 𝔼 X and a random vector y = Y with finite second moments, when the covariance matrix of X has the form A * T * A.

The hypothesis on the covariance forces the centred variable into the range of A almost surely, which is what allows A to be singular: the mean of ‖(1 - A * A⁺) (X - 𝔼 X)‖ ^ 2 is a trace against the covariance that vanishes.

Main statements

• TauCeti.ae_sub_integral_mem_range_toEuclideanLin: if the covariance matrix of X has the form A * T, the centred variable lies almost surely in the range of A.
• TauCeti.integral_inner_sub_integral_le: the quadratic Fenchel–Young inequality in mean, for a random vector whose covariance has the form A * T * A.

theorem TauCeti.ae_sub_integral_mem_range_toEuclideanLin {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → EuclideanSpace ℝ ι} (hX : MeasureTheory.MemLp X 2 P) {A T : Matrix ι ι ℝ} (hA : A.PosSemidef) (hcov : covMatrix (MeasureTheory.Measure.map X P) = A * T) : ∀ᵐ (ω : Ω) ∂P, X ω - ∫ (ω' : Ω), X ω' ∂P ∈ (Matrix.toEuclideanLin A).range

The centred variable lies in the range of the covariance. If the covariance matrix of a square-integrable random vector X has the form A * T for a positive-semidefinite matrix A, then X - 𝔼 X lies almost surely in the range of A.

theorem TauCeti.integral_inner_sub_integral_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → EuclideanSpace ℝ ι} (hX : MeasureTheory.MemLp X 2 P) (hY : MeasureTheory.MemLp Y 2 P) {A T : Matrix ι ι ℝ} (hA : A.PosSemidef) (hcov : covMatrix (MeasureTheory.Measure.map X P) = A * T * A) : ∫ (ω : Ω), inner ℝ (X ω - ∫ (ω' : Ω), X ω' ∂P) (Y ω) ∂P ≤ (∫ (ω : Ω), inner ℝ ((Matrix.toEuclideanLin A) (Y ω)) (Y ω) ∂P + (A * T).trace) / 2

The quadratic Fenchel–Young inequality in mean. Let X and Y be square-integrable random vectors, where the law of X has covariance matrix A * T * A for a positive-semidefinite matrix A. Then the correlation of the centred variable X - 𝔼 X with Y is at most (𝔼 ⟪A Y, Y⟫ + tr (A * T)) / 2.