feat: covarianceBilin of the push-forward measure

Mathlib/Probability/Moments/Basic.lean

@@ -480,3 +480,27 @@ lemma integrable_exp_mul_of_mem_Icc [IsFiniteMeasure μ] {X : Ω → ℝ} {a b t
   · exact ⟨Or.inr (by nlinarith), Or.inl (by nlinarith)⟩
 
 end ProbabilityTheory
+
+namespace ContinuousLinearMap
+
+variable {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F]
+    [NormedSpace 𝕜 E] [NormedSpace ℝ E] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [CompleteSpace E]
+    [CompleteSpace F] [MeasurableSpace E] {μ : Measure E}
+
+lemma integral_comp_id_comm' (h : Integrable id μ) (L : E →L[𝕜] F) :
+    μ[L] = L μ[id] := by
+  change ∫ x, L (id x) ∂μ = _
+  rw [L.integral_comp_comm h]
+
+lemma integral_comp_id_comm (h : Integrable id μ) (L : E →L[𝕜] F) :
+    μ[L] = L (∫ x, x ∂μ) :=
+  L.integral_comp_id_comm' h
+
+variable [OpensMeasurableSpace E] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F]
+
+lemma integral_id_map (h : Integrable id μ) (L : E →L[𝕜] F) :
+    ∫ x, x ∂(μ.map L) = L (∫ x, x ∂μ) := by
+  rw [integral_map (by fun_prop) (by fun_prop)]
+  simp [L.integral_comp_id_comm h]
+
+end ContinuousLinearMap

Mathlib/Probability/Moments/CovarianceBilin.lean

@@ -1,3 +1,171 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Etienne Marion
+-/
+import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.CovarianceBilinDual
 
-deprecated_module (since := "2025-10-13")
+/-!
+# Covariance in Hilbert spaces
+
+Given a measure `μ` defined over a Banach space `E`, one can consider the associated covariance
+bilinear form which maps `L₁ L₂ : StrongDual ℝ E` to `cov[L₁, L₂; μ]`. This is called
+`covarianceBilinDual μ` and is defined in the `CovarianceBilinDual` file.
+
+In the special case where `E` is a Hilbert space, each `L : StrongDual ℝ E` can be represented
+as the scalar product against some element of `E`. This motivates the definition of
+`covarianceBilin`, which is a continuous bilinear form mapping `x y : E` to
+`cov[⟪x, ·⟫, ⟪y, ·⟫; μ]`.
+
+## Main definition
+
+* `covarianceBilin μ`: the continuous bilinear form over `E` representing the covariance of a
+  measure over `E`.
+
+## Tags
+
+covariance, Hilbert space, bilinear form
+-/
+
+open MeasureTheory InnerProductSpace NormedSpace WithLp EuclideanSpace
+
+namespace ProbabilityTheory
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
+
+/-- Covariance of a measure on an inner product space, as a continuous bilinear form. -/
+noncomputable
+def covarianceBilin (μ : Measure E) : E →L[ℝ] E →L[ℝ] ℝ :=
+  ContinuousLinearMap.bilinearComp (covarianceBilinDual μ)
+    (toDualMap ℝ E).toContinuousLinearMap (toDualMap ℝ E).toContinuousLinearMap
+
+@[simp]
+lemma covarianceBilin_zero : covarianceBilin (0 : Measure E) = 0 := by
+  rw [covarianceBilin]
+  simp
+
+lemma covarianceBilin_eq_covarianceBilinDual (x y : E) :
+    covarianceBilin μ x y = covarianceBilinDual μ (toDualMap ℝ E x) (toDualMap ℝ E y) := rfl
+
+@[simp]
+lemma covarianceBilin_of_not_memLp [IsFiniteMeasure μ] (h : ¬MemLp id 2 μ) :
+    covarianceBilin μ = 0 := by
+  ext
+  simp [covarianceBilin_eq_covarianceBilinDual, h]
+
+lemma covarianceBilin_apply [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
+    covarianceBilin μ x y = ∫ z, ⟪x, z - μ[id]⟫_ℝ * ⟪y, z - μ[id]⟫_ℝ ∂μ := by
+  simp_rw [covarianceBilin, ContinuousLinearMap.bilinearComp_apply, covarianceBilinDual_apply' h]
+  simp only [LinearIsometry.coe_toContinuousLinearMap, id_eq, toDualMap_apply]
+
+lemma covarianceBilin_comm [IsFiniteMeasure μ] (x y : E) :
+    covarianceBilin μ x y = covarianceBilin μ y x := by
+  rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
+    covarianceBilin_eq_covarianceBilinDual]
+
+lemma covarianceBilin_self [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : E) :
+    covarianceBilin μ x x = Var[fun u ↦ ⟪x, u⟫_ℝ; μ] := by
+  rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_self_eq_variance h]
+  rfl
+
+lemma covarianceBilin_apply_eq_cov [CompleteSpace E] [IsFiniteMeasure μ]
+    (h : MemLp id 2 μ) (x y : E) :
+    covarianceBilin μ x y = cov[fun u ↦ ⟪x, u⟫_ℝ, fun u ↦ ⟪y, u⟫_ℝ; μ] := by
+  rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_eq_covariance h]
+  rfl
+
+lemma covarianceBilin_real {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : ℝ) :
+    covarianceBilin μ x y = x * y * Var[id; μ] := by
+  simp only [covarianceBilin_apply_eq_cov h, RCLike.inner_apply, conj_trivial, mul_comm]
+  rw [covariance_mul_left, covariance_mul_right, ← mul_assoc, covariance_self aemeasurable_id']
+  rfl
+
+lemma covarianceBilin_real_self {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : ℝ) :
+    covarianceBilin μ x x = x ^ 2 * Var[id; μ] := by
+  rw [covarianceBilin_real h, pow_two]
+
+@[simp]
+lemma covarianceBilin_self_nonneg [CompleteSpace E] [IsFiniteMeasure μ] (x : E) :
+    0 ≤ covarianceBilin μ x x := by
+  simp [covarianceBilin]
+
+lemma isPosSemidef_covarianceBilin [CompleteSpace E] [IsFiniteMeasure μ] :
+    (covarianceBilin μ).toBilinForm.IsPosSemidef where
+  eq := covarianceBilin_comm
+  nonneg := covarianceBilin_self_nonneg
+
+lemma covarianceBilin_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+    [MeasurableSpace F] [BorelSpace F] [CompleteSpace E] [FiniteDimensional ℝ F]
+    [IsFiniteMeasure μ] (h : MemLp id 2 μ) (L : E →L[ℝ] F) (u v : F) :
+    covarianceBilin (μ.map L) u v = covarianceBilin μ (L.adjoint u) (L.adjoint v) := by
+  rw [covarianceBilin_apply, covarianceBilin_apply h]
+  · simp_rw [id, L.integral_id_map (h.integrable (by simp))]
+    rw [integral_map]
+    · simp_rw [← map_sub, ← L.adjoint_inner_left]
+    all_goals fun_prop
+  · exact memLp_map_measure_iff (by fun_prop) (by fun_prop) |>.2 (L.comp_memLp' h)
+
+lemma covarianceBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] (c : E) :
+    covarianceBilin (μ.map (fun x ↦ c + x)) = covarianceBilin μ := by
+  by_cases h : MemLp id 2 μ
+  · ext x y
+    have h_Lp : MemLp id 2 (μ.map (fun x ↦ c + x)) :=
+      (measurableEmbedding_addLeft _).memLp_map_measure_iff.mpr <| (memLp_const c).add h
+    rw [covarianceBilin_apply h_Lp,
+      covarianceBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
+    congr with z
+    rw [integral_map (by fun_prop) h_Lp.1]
+    simp only [id_eq]
+    rw [integral_add (integrable_const _)]
+    · simp
+    · exact h.integrable (by simp)
+  · ext
+    rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h]
+    rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
+    contrapose! h
+    convert (memLp_const (-c)).add h
+    ext; simp
+
+lemma covarianceBilin_apply_basisFun {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i j : ι) :
+    covarianceBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+      (basisFun ι ℝ i) (basisFun ι ℝ j) = cov[X i, X j; μ] := by
+  have (i : ι) := (hX i).aemeasurable
+  rw [covarianceBilin_apply_eq_cov, covariance_map]
+  · simp [basisFun_inner]; rfl
+  · exact Measurable.aestronglyMeasurable (by fun_prop)
+  · exact Measurable.aestronglyMeasurable (by fun_prop)
+  · fun_prop
+  · exact (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 (MemLp.of_eval_piLp hX)
+
+lemma covarianceBilin_apply_basisFun_self {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i : ι) :
+    covarianceBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+      (basisFun ι ℝ i) (basisFun ι ℝ i) = Var[X i; μ] := by
+  rw [covarianceBilin_apply_basisFun hX, covariance_self]
+  have (i : ι) := (hX i).aemeasurable
+  fun_prop
+
+lemma covarianceBilin_apply_pi {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ}
+    (hX : ∀ i, MemLp (X i) 2 μ) (x y : EuclideanSpace ℝ ι) :
+    covarianceBilin (μ.map (fun ω ↦ toLp 2 (X · ω))) x y =
+      ∑ i, ∑ j, x i * y j * cov[X i, X j; μ] := by
+  have (i : ι) := (hX i).aemeasurable
+  nth_rw 1 [covarianceBilin_apply_eq_cov, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
+    ← (basisFun ι ℝ).sum_repr' y]
+  · simp_rw [sum_inner, real_inner_smul_left, basisFun_inner, PiLp.toLp_apply]
+    rw [covariance_fun_sum_fun_sum]
+    · refine Finset.sum_congr rfl fun i _ ↦ Finset.sum_congr rfl fun j _ ↦ ?_
+      rw [covariance_mul_left, covariance_mul_right]
+      ring
+    all_goals exact fun i ↦ (hX i).const_mul _
+  any_goals exact Measurable.aestronglyMeasurable (by fun_prop)
+  · fun_prop
+  · exact (memLp_map_measure_iff aestronglyMeasurable_id (by fun_prop)).2 (MemLp.of_eval_piLp hX)
+
+end ProbabilityTheory

Mathlib/Probability/Moments/CovarianceBilinDual.lean

@@ -291,6 +291,13 @@ lemma covarianceBilinDual_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual 
 @[deprecated (since := "2025-07-16")] alias covarianceBilin_same_eq_variance :=
   covarianceBilinDual_self_eq_variance
 
+@[simp]
+lemma covarianceBilinDual_self_nonneg (L : StrongDual ℝ E) : 0 ≤ covarianceBilinDual μ L L := by
+  by_cases h : MemLp id 2 μ
+  · rw [covarianceBilinDual_self_eq_variance h]
+    exact variance_nonneg ..
+  · simp [h]
+
 end Covariance
 
 end ProbabilityTheory

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -502,7 +502,7 @@ variable {𝕜 𝕜₂ 𝕜₃ : Type*} [NormedField 𝕜] [NormedField 𝕜₂]
   [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G]
   {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
 
-/-- Send a continuous bilinear map to an abstract bilinear map (forgetting continuity). -/
+/-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
 def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G :=
   (coeLMₛₗ σ₂₃).comp L.toLinearMap
 
@@ -513,6 +513,12 @@ def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[
 
 @[deprecated (since := "2025-07-28")] alias toLinearMap₂_apply := toLinearMap₁₂_apply
 
+/-- Send a continuous bilinear form to an abstract bilinear form (forgetting continuity). -/
+def toBilinForm (L : E →L[𝕜] E →L[𝕜] 𝕜) : LinearMap.BilinForm 𝕜 E := L.toLinearMap₁₂
+
+@[simp] lemma toBilinForm_apply (L : E →L[𝕜] E →L[𝕜] 𝕜) (v : E) (w : E) :
+    L.toBilinForm v w = L v w := rfl
+
 end BilinearMaps
 
 section RestrictScalars