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).
• covarianceBilin : 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 covarianceBilin μ = 0.

Main statements

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

Implementation notes

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

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

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

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

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

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 := ⋯ }

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

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

noncomputable 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[ℝ] ℝ

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 μ = ⋯.toContinuousLinearMap.bilinearComp (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)

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) : ((uncenteredCovarianceBilin μ) L₁) L₂ = ∫ (x : E), L₁ x * L₂ x ∂μ

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) : ((uncenteredCovarianceBilin μ) L₁) L₂ = 0

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

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) : ‖((uncenteredCovarianceBilin μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

noncomputable def ProbabilityTheory.covarianceBilin {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.covarianceBilin μ = ProbabilityTheory.uncenteredCovarianceBilin (MeasureTheory.Measure.map (fun (x : E) => x - ∫ (x : E), x ∂μ) μ)

@[simp]

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L₁) L₂ = 0

@[simp]

theorem ProbabilityTheory.covarianceBilin_zero {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} [NormedSpace ℝ E] [BorelSpace E] : covarianceBilin 0 = 0

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

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L₁) L₂ = ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L₁) L₂ = ∫ (x : E), L₁ (x - ∫ (x : E), id x ∂μ) * L₂ (x - ∫ (x : E), id x ∂μ) ∂μ

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L₁) L₂ = covariance (⇑L₁) (⇑L₂) μ

theorem ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L) L = variance (⇑L) μ

@[deprecated ProbabilityTheory.covarianceBilin_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) : ((covarianceBilin μ) L) L = variance (⇑L) μ

Alias of ProbabilityTheory.covarianceBilin_self_eq_variance.