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

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

StrongDual.toLpₗ μ p = if h_Lp : MeasureTheory.MemLp id p μ then { toFun := fun (L : StrongDual 𝕜 E) => MeasureTheory.MemLp.toLp ⇑L ⋯, map_add' := ⋯, map_smul' := ⋯ } else 0

Instances For

source

@[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

@[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

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

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

StrongDual.toLp μ p = { toLinearMap := StrongDual.toLpₗ μ p, cont := ⋯ }

Instances For

source

@[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

@[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

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

ProbabilityTheory.uncenteredCovarianceBilinDual μ = ⋯.toContinuousLinearMap.bilinearComp (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)

Instances For

source

@[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

@ProbabilityTheory.uncenteredCovarianceBilin = @ProbabilityTheory.uncenteredCovarianceBilinDual

Instances For

source

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

@[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

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

@[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

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

uncenteredCovarianceBilinDual 0 = 0

source

@[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

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

@[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

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

ProbabilityTheory.covarianceBilinDual μ = ProbabilityTheory.uncenteredCovarianceBilinDual (MeasureTheory.Measure.map (fun (x : E) => x - ∫ (x : E), x ∂μ) μ)

Instances For

source

@[simp]

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

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

source

@[simp]

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

covarianceBilinDual 0 = 0

source

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

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

source

theorem ProbabilityTheory.covarianceBilinDual_apply {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [MeasureTheory.IsFiniteMeasure μ] [CompleteSpace E] (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

theorem ProbabilityTheory.covarianceBilinDual_apply' {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [BorelSpace E] [MeasureTheory.IsFiniteMeasure μ] [CompleteSpace E] (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

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

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

source

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

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

source

@[deprecated ProbabilityTheory.covarianceBilinDual_self_eq_variance (since := "2025-07-16")]

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

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

Alias of ProbabilityTheory.covarianceBilinDual_self_eq_variance.

Documentation

Mathlib.Probability.Moments.CovarianceBilinDual

Covariance in Banach spaces #

Main definitions #

Main statements #

Implementation notes #