Covariance in Banach spaces #

We define the covariance of a finite measure in a Banach space E, as a continuous bilinear form on Dual ℝ E.

Main definitions #

Let μ be a finite measure on a normed space E with the Borel σ-algebra. We then define

Dual.toLp: the function MemLp.toLp as a continuous linear map from Dual 𝕜 E (for RCLike 𝕜) into the space Lp 𝕜 p μ for p ≥ 1. This needs a hypothesis MemLp id p μ (we set it to the junk value 0 if that's not the case).
covarianceBilinDual : covariance of a measure μ with ∫ x, ‖x‖^2 ∂μ < ∞ on a Banach space, as a continuous bilinear form Dual ℝ E →L[ℝ] Dual ℝ E →L[ℝ] ℝ. If the second moment of μ is not finite, we set covarianceBilinDual μ = 0.

Main statements #

covarianceBilinDual_apply : the covariance of μ on L₁, L₂ : Dual ℝ E is equal to ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ.
covarianceBilinDual_same_eq_variance: covarianceBilinDual μ L L = Var[L; μ].

Implementation notes #

The hypothesis that μ has a second moment is written as MemLp id 2 μ in the code.

source

🔸 coverage

noncomputable def StrongDual.toLpₗ {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (μ : MeasureTheory.Measure E) (p : ENNReal) :

StrongDual 𝕜 E →ₗ[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)

Linear map from the dual to Lp equal to MemLp.toLp if MemLp id p μ and to 0 otherwise.

Equations

Instances For

source

📐 coverage

@[simp]

theorem StrongDual.toLpₗ_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (h_Lp : MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E) :

(toLpₗ μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯

source

📐 coverage

@[simp]

theorem StrongDual.toLpₗ_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (h_Lp : ¬MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E) :

(toLpₗ μ p) L = 0

source

📐 coverage

theorem StrongDual.norm_toLpₗ_le {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [OpensMeasurableSpace E] (L : StrongDual 𝕜 E) :

‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (MeasureTheory.eLpNorm id p μ).toReal

source

🔸 coverage

noncomputable def StrongDual.toLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) (p : ENNReal) [Fact (1 ≤ p)] :

StrongDual 𝕜 E →L[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)

Continuous linear map from the dual to Lp equal to MemLp.toLp if MemLp id p μ and to 0 otherwise.

Equations

Instances For

source

📐 coverage

@[simp]

theorem StrongDual.toLp_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal} {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [OpensMeasurableSpace E] [Fact (1 ≤ p)] (h_Lp : MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E) :

(toLp μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯

source

📐 coverage

@[simp]

theorem StrongDual.toLp_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {p : ENNReal} {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [OpensMeasurableSpace E] [Fact (1 ≤ p)] (h_Lp : ¬MeasureTheory.MemLp id p μ) (L : StrongDual 𝕜 E) :

(toLp μ p) L = 0

source

🔸 coverage

noncomputable def ProbabilityTheory.uncenteredCovarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) :

StrongDual ℝ E →L[ℝ ] StrongDual ℝ E →L[ℝ ] ℝ

Continuous bilinear form with value ∫ x, L₁ x * L₂ x ∂μ on (L₁, L₂). This is equal to the covariance only if μ is centered.

Equations

Instances For

source

🔸 coverage

@[deprecated ProbabilityTheory.uncenteredCovarianceBilinDual (since := "2025-10-10")]

def ProbabilityTheory.uncenteredCovarianceBilin {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) :

StrongDual ℝ E →L[ℝ ] StrongDual ℝ E →L[ℝ ] ℝ

Alias of ProbabilityTheory.uncenteredCovarianceBilinDual.

Continuous bilinear form with value ∫ x, L₁ x * L₂ x ∂μ on (L₁, L₂). This is equal to the covariance only if μ is centered.

Equations

Instances For

source

📐 coverage

theorem ProbabilityTheory.uncenteredCovarianceBilinDual_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((uncenteredCovarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ x * L₂ x ∂μ

source

📐 coverage

@[deprecated ProbabilityTheory.uncenteredCovarianceBilinDual_apply (since := "2025-10-10")]

theorem ProbabilityTheory.uncenteredCovarianceBilin_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((uncenteredCovarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ x * L₂ x ∂μ

Alias of ProbabilityTheory.uncenteredCovarianceBilinDual_apply.

source

📐 coverage

theorem ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (h : ¬MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((uncenteredCovarianceBilinDual μ) L₁) L₂ = 0

source

📐 coverage

@[deprecated ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp (since := "2025-10-10")]

theorem ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (h : ¬MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((uncenteredCovarianceBilinDual μ) L₁) L₂ = 0

Alias of ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp.

source

📐 coverage

@[simp]

theorem ProbabilityTheory.uncenteredCovarianceBilinDual_zero {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [OpensMeasurableSpace E] :

uncenteredCovarianceBilinDual 0 = 0

source

📐 coverage

@[deprecated ProbabilityTheory.uncenteredCovarianceBilinDual_zero (since := "2025-10-10")]

theorem ProbabilityTheory.uncenteredCovarianceBilin_zero {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [OpensMeasurableSpace E] :

uncenteredCovarianceBilinDual 0 = 0

Alias of ProbabilityTheory.uncenteredCovarianceBilinDual_zero.

source

📐 coverage

theorem ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (L₁ L₂ : StrongDual ℝ E) :

‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

source

📐 coverage

@[deprecated ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le (since := "2025-10-10")]

theorem ProbabilityTheory.norm_uncenteredCovarianceBilin_le {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (L₁ L₂ : StrongDual ℝ E) :

‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Alias of ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le.

source

🔸 coverage

noncomputable def ProbabilityTheory.covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [BorelSpace E] (μ : MeasureTheory.Measure E) :

StrongDual ℝ E →L[ℝ ] StrongDual ℝ E →L[ℝ ] ℝ

Continuous bilinear form with value ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ on (L₁, L₂) if MemLp id 2 μ. If not, we set it to zero.

Equations

Instances For

source

theorem MeasureTheory.memLp_id_of_self_sub_integral {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : Measure E} [NormedSpace ℝ E] {p : ENNReal} (h_Lp : MemLp (fun (x : E) => x - ∫ (y : E), y ∂μ) p μ) :

MemLp id p μ

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_of_not_memLp' {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] (h : ¬MeasureTheory.MemLp (fun (x : E) => x - ∫ (y : E), y ∂μ) 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = 0

source

📐 coverage

@[simp]

theorem ProbabilityTheory.covarianceBilinDual_of_not_memLp {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] (h : ¬MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = 0

source

📐 coverage

@[simp]

theorem ProbabilityTheory.covarianceBilinDual_zero {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [BorelSpace E] :

covarianceBilinDual 0 = 0

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_comm {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁

source

📐 coverage

@[simp]

theorem ProbabilityTheory.covarianceBilinDual_self_nonneg {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] (L : StrongDual ℝ E) :

0 ≤ ((covarianceBilinDual μ) L) L

source

📐 coverage

theorem ProbabilityTheory.isPosSemidef_covarianceBilinDual {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] :

(covarianceBilinDual μ).toBilinForm.IsPosSemidef

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_apply' {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_eq_covariance {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :

((covarianceBilinDual μ) L₁) L₂ = covariance (⇑L₁) (⇑L₂) μ

source

📐 coverage

theorem ProbabilityTheory.covarianceBilinDual_self_eq_variance {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L : StrongDual ℝ E) :

((covarianceBilinDual μ) L) L = variance (⇑L) μ

Documentation

Mathlib.Probability.Moments.CovarianceBilinDual

Covariance in Banach spaces #

Main definitions #

Main statements #

Implementation notes #