# 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
@[simp]
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
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
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
@[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
@[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] (L₁ L₂ : StrongDual ℝ E) :
((covarianceBilinDual μ) L₁) L₂ = ((covarianceBilinDual μ) L₂) L₁
source
@[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
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
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
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
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) μ
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] [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (h : MeasureTheory.MemLp id 2 μ) (L : StrongDual ℝ E) :
((covarianceBilinDual μ) L) L = variance (⇑L) μ

Alias of `ProbabilityTheory.covarianceBilinDual_self_eq_variance`.