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 NormedSpace.Dual.toLpₗ {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (μ : MeasureTheory.Measure E) (p : ENNReal) : Dual 𝕜 E →ₗ[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)

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

Equations

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

@[simp]

theorem NormedSpace.Dual.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 : Dual 𝕜 E) : (toLpₗ μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯

@[simp]

theorem NormedSpace.Dual.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 : Dual 𝕜 E) : (toLpₗ μ p) L = 0

theorem NormedSpace.Dual.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 : Dual 𝕜 E) : ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (MeasureTheory.eLpNorm id p μ).toReal

noncomputable def NormedSpace.Dual.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)] : Dual 𝕜 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

• NormedSpace.Dual.toLp μ p = { toLinearMap := NormedSpace.Dual.toLpₗ μ p, cont := ⋯ }

@[simp]

theorem NormedSpace.Dual.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 : Dual 𝕜 E) : (toLp μ p) L = MeasureTheory.MemLp.toLp ⇑L ⋯

@[simp]

theorem NormedSpace.Dual.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 : Dual 𝕜 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) : NormedSpace.Dual ℝ E →L[ℝ] NormedSpace.Dual ℝ 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 (NormedSpace.Dual.toLp μ 2) (NormedSpace.Dual.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₂ : NormedSpace.Dual ℝ 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₂ : NormedSpace.Dual ℝ E) : ((uncenteredCovarianceBilin μ) L₁) L₂ = 0

theorem ProbabilityTheory.norm_uncenteredCovarianceBilin_le {E : Type u_1} [NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [NormedSpace ℝ E] [OpensMeasurableSpace E] (L₁ L₂ : NormedSpace.Dual ℝ 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) : NormedSpace.Dual ℝ E →L[ℝ] NormedSpace.Dual ℝ 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₂ : NormedSpace.Dual ℝ E) : ((covarianceBilin μ) L₁) L₂ = 0

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

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 : NormedSpace.Dual ℝ E) : ((covarianceBilin μ) L) L = variance (⇑L) μ