From af4d6abe6d80cc8e7ac88514f3d31823fe1a7e49 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Wed, 8 Oct 2025 13:27:52 +0200
Subject: [PATCH 01/28] feat: introduce covInnerBilin

---
 .../Probability/Moments/CovInnerBilin.lean    | 139 ++++++++++++++++++
 .../Probability/Moments/CovarianceBilin.lean  |   8 +
 .../Algebra/Module/StrongTopology.lean        |   8 +-
 3 files changed, 154 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/Probability/Moments/CovInnerBilin.lean

diff --git a/Mathlib/Probability/Moments/CovInnerBilin.lean b/Mathlib/Probability/Moments/CovInnerBilin.lean
new file mode 100644
index 00000000000000..b9a07bf073c9f8
--- /dev/null
+++ b/Mathlib/Probability/Moments/CovInnerBilin.lean
@@ -0,0 +1,139 @@
+/-
+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.Dual
+import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.CovarianceBilin
+
+/-!
+# Covariance matrix
+
+-/
+
+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 covInnerBilin (μ : Measure E) : E →L[ℝ] E →L[ℝ] ℝ :=
+  ContinuousLinearMap.bilinearComp (covarianceBilin μ)
+    (toDualMap ℝ E).toContinuousLinearMap (toDualMap ℝ E).toContinuousLinearMap
+
+@[simp]
+lemma covInnerBilin_zero : covInnerBilin (0 : Measure E) = 0 := by
+  rw [covInnerBilin]
+  simp
+
+lemma covInnerBilin_eq_covarianceBilin (x y : E) :
+    covInnerBilin μ x y = covarianceBilin μ (toDualMap ℝ E x) (toDualMap ℝ E y) := rfl
+
+@[simp]
+lemma covInnerBilin_of_not_memLp [IsFiniteMeasure μ] (h : ¬MemLp id 2 μ) :
+    covInnerBilin μ = 0 := by
+  ext
+  simp [covInnerBilin_eq_covarianceBilin, h]
+
+lemma covInnerBilin_apply [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
+    covInnerBilin μ x y = ∫ z, ⟪x, z - μ[id]⟫_ℝ * ⟪y, z - μ[id]⟫_ℝ ∂μ := by
+  simp_rw [covInnerBilin, ContinuousLinearMap.bilinearComp_apply, covarianceBilin_apply' h]
+  simp only [LinearIsometry.coe_toContinuousLinearMap, id_eq, toDualMap_apply]
+
+lemma covInnerBilin_comm [IsFiniteMeasure μ] (x y : E) :
+    covInnerBilin μ x y = covInnerBilin μ y x := by
+  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_comm, covInnerBilin_eq_covarianceBilin]
+
+lemma covInnerBilin_self [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : E) :
+    covInnerBilin μ x x = Var[fun u ↦ ⟪x, u⟫_ℝ; μ] := by
+  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_self_eq_variance h]
+  rfl
+
+lemma covInnerBilin_apply_eq [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
+    covInnerBilin μ x y = cov[fun u ↦ ⟪x, u⟫_ℝ, fun u ↦ ⟪y, u⟫_ℝ; μ] := by
+  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_eq_covariance h]
+  rfl
+
+lemma covInnerBilin_real {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : ℝ) :
+    covInnerBilin μ x y = x * y * Var[id; μ] := by
+  simp only [covInnerBilin_apply_eq h, RCLike.inner_apply, conj_trivial, mul_comm]
+  rw [covariance_mul_left, covariance_mul_right, ← mul_assoc, covariance_self aemeasurable_id']
+  rfl
+
+lemma covInnerBilin_real_self {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : ℝ) :
+    covInnerBilin μ x x = x ^ 2 * Var[id; μ] := by
+  rw [covInnerBilin_real h, pow_two]
+
+@[simp]
+lemma covInnerBilin_self_nonneg [CompleteSpace E] [IsFiniteMeasure μ] (x : E) :
+    0 ≤ covInnerBilin μ x x := by
+  simp [covInnerBilin]
+
+lemma isPosSemidef_covInnerBilin [CompleteSpace E] [IsFiniteMeasure μ] :
+    (covInnerBilin μ).toBilinForm.IsPosSemidef where
+  eq := covInnerBilin_comm
+  nonneg := covInnerBilin_self_nonneg
+
+lemma covInnerBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] (c : E) :
+    covInnerBilin (μ.map (fun x ↦ c + x)) = covInnerBilin μ := 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 [covInnerBilin_apply h_Lp, covInnerBilin_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 [covInnerBilin_of_not_memLp, covInnerBilin_of_not_memLp h]
+    rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not]
+    contrapose! h
+    convert (memLp_const (-c)).add h
+    ext; simp
+
+lemma covInnerBilin_apply_basisFun {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i j : ι) :
+    covInnerBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+      (basisFun ι ℝ i) (basisFun ι ℝ j) = cov[X i, X j; μ] := by
+  have (i : ι) := (hX i).aemeasurable
+  rw [covInnerBilin_apply_eq, 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 covInnerBilin_apply_basisFun_self {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i : ι) :
+    covInnerBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+      (basisFun ι ℝ i) (basisFun ι ℝ i) = Var[X i; μ] := by
+  rw [covInnerBilin_apply_basisFun hX, covariance_self]
+  have (i : ι) := (hX i).aemeasurable
+  fun_prop
+
+lemma covInnerBilin_apply_pi {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+    {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ}
+    (hX : ∀ i, MemLp (X i) 2 μ) (x y : EuclideanSpace ℝ ι) :
+    covInnerBilin (μ.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 [covInnerBilin_apply_eq, 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
diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index 4dc3b4dbbb90cc..b8b737a54a6a0f 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -273,6 +273,14 @@ lemma covarianceBilin_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual ℝ E
     covarianceBilin μ L L = Var[L; μ] := by
   rw [covarianceBilin_eq_covariance h, covariance_self (by fun_prop)]
 
+@[simp]
+lemma covarianceBilin_self_nonneg (L : StrongDual ℝ E) :
+    0 ≤ covarianceBilin μ L L := by
+  by_cases h : MemLp id 2 μ
+  · rw [covarianceBilin_self_eq_variance h]
+    exact variance_nonneg ..
+  · simp [h]
+
 @[deprecated (since := "2025-07-16")] alias covarianceBilin_same_eq_variance :=
   covarianceBilin_self_eq_variance
 
diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean
index 45905214e6761e..a75e0cbaa42e28 100644
--- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean
+++ b/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

From 9b43241b57888961d0bc6a9fd7227600cefef112 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?=
 <4094732+RemyDegenne@users.noreply.github.com>
Date: Wed, 8 Oct 2025 13:33:51 +0200
Subject: [PATCH 02/28] =?UTF-8?q?add=20R=C3=A9my=20as=20coauthor?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit


From 4064e613fd13d140e0e1fd08ca0bbb251660edd8 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Wed, 8 Oct 2025 14:16:11 +0200
Subject: [PATCH 03/28] mk_all

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 1677e7714ce2f9..7a89d7c0bfef4d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5356,6 +5356,7 @@ import Mathlib.Probability.Martingale.OptionalStopping
 import Mathlib.Probability.Martingale.Upcrossing
 import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.ComplexMGF
+import Mathlib.Probability.Moments.CovInnerBilin
 import Mathlib.Probability.Moments.Covariance
 import Mathlib.Probability.Moments.CovarianceBilin
 import Mathlib.Probability.Moments.IntegrableExpMul

From 1b00af05d222d1a98d385d25a1ebb1b2e589e56e Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Wed, 8 Oct 2025 14:24:56 +0200
Subject: [PATCH 04/28] module docstring

---
 Mathlib/Probability/Moments/CovInnerBilin.lean | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments/CovInnerBilin.lean b/Mathlib/Probability/Moments/CovInnerBilin.lean
index b9a07bf073c9f8..996b91305fdef5 100644
--- a/Mathlib/Probability/Moments/CovInnerBilin.lean
+++ b/Mathlib/Probability/Moments/CovInnerBilin.lean
@@ -8,8 +8,24 @@ import Mathlib.MeasureTheory.SpecificCodomains.WithLp
 import Mathlib.Probability.Moments.CovarianceBilin
 
 /-!
-# Covariance matrix
+# 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
+`CovarianceBilin μ` and is defined in the `CovarianceBilin` 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 `covInnerBilin`,
+which is bilinear form mapping `x y : E` to `cov[⟪x, ·⟫, ⟪y, ·⟫; μ]`.
+
+## Main definition
+
+* `covInnerBilin μ`: 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

From 78cdfda21b9c1b2e190a6fc65e4fa35525e65b8e Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:02:40 +0200
Subject: [PATCH 05/28] rfc: make ContinuousLinearMap protected

---
 Mathlib/Topology/Algebra/Module/LinearMap.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index 7f55f98e690db9..3d8fe551739119 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -313,11 +313,13 @@ section
 variable (R₁ M₁)
 
 /-- the identity map as a continuous linear map. -/
-def id : M₁ →L[R₁] M₁ :=
+protected def id : M₁ →L[R₁] M₁ :=
   ⟨LinearMap.id, continuous_id⟩
 
 end
 
+open ContinuousLinearMap (id)
+
 instance one : One (M₁ →L[R₁] M₁) :=
   ⟨id R₁ M₁⟩
 
@@ -757,6 +759,8 @@ end ToSpanSingleton
 
 end Semiring
 
+open ContinuousLinearMap (id)
+
 section Ring
 
 variable {R : Type*} [Ring R] {R₂ : Type*} [Ring R₂] {R₃ : Type*} [Ring R₃] {M : Type*}
@@ -1123,6 +1127,8 @@ end RestrictScalars
 
 end ContinuousLinearMap
 
+open ContinuousLinearMap (id)
+
 namespace Submodule
 
 variable {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]

From 9741ee2fe7eaf718248105267f95b4ae2609e08a Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:16:24 +0200
Subject: [PATCH 06/28] fix

---
 Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
index bf47036bef1f5a..a51a3896f50223 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
@@ -14,6 +14,7 @@ assert_not_exists TrivialStar
 
 open LinearMap (ker range)
 open Topology Filter Pointwise
+open ContinuousLinearMap (id)
 
 universe u v w u'
 

From 5450bf04a752592520e882f277d031a3fc65222a Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:21:43 +0200
Subject: [PATCH 07/28] fix

---
 Mathlib/Topology/Algebra/Module/Equiv.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean
index ad8ccc967797b7..00e9e8db493c07 100644
--- a/Mathlib/Topology/Algebra/Module/Equiv.lean
+++ b/Mathlib/Topology/Algebra/Module/Equiv.lean
@@ -1028,6 +1028,8 @@ end ContinuousLinearEquiv
 
 namespace ContinuousLinearMap
 
+open ContinuousLinearMap (id)
+
 variable {R : Type*} {M M₂ M₃ : Type*}
   [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃]
 

From 95fd04d060e7eb238f50b7688c4c5f6668282295 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:37:28 +0200
Subject: [PATCH 08/28] fix

---
 Mathlib/Analysis/Normed/Operator/Basic.lean     | 1 +
 Mathlib/Analysis/Normed/Operator/Conformal.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean
index 3a5bd8c1680630..249e086178c811 100644
--- a/Mathlib/Analysis/Normed/Operator/Basic.lean
+++ b/Mathlib/Analysis/Normed/Operator/Basic.lean
@@ -38,6 +38,7 @@ variable {𝕜 𝕜₂ 𝕜₃ E F Fₗ G 𝓕 : Type*}
 section SemiNormed
 
 open Metric ContinuousLinearMap
+open ContinuousLinearMap (id)
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup Fₗ]
   [SeminormedAddCommGroup G]
diff --git a/Mathlib/Analysis/Normed/Operator/Conformal.lean b/Mathlib/Analysis/Normed/Operator/Conformal.lean
index 840cdd2ce6c32a..a59e711f2a6d2b 100644
--- a/Mathlib/Analysis/Normed/Operator/Conformal.lean
+++ b/Mathlib/Analysis/Normed/Operator/Conformal.lean
@@ -41,7 +41,7 @@ The definition of conformality in this file does NOT require the maps to be orie
 noncomputable section
 
 open Function LinearIsometry ContinuousLinearMap
-
+open ContinuousLinearMap (id)
 
 /-- A continuous linear map `f'` is said to be conformal if it's
 a nonzero multiple of a linear isometry. -/

From 3f57716cfb097d3e1ceed492660ab977d0b5ba7f Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:45:11 +0200
Subject: [PATCH 09/28] fix

---
 Mathlib/Analysis/Calculus/FDeriv/Basic.lean    | 1 +
 Mathlib/Analysis/Normed/Operator/Basic.lean    | 2 +-
 Mathlib/Analysis/Normed/Operator/Bilinear.lean | 3 ++-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
index fc78c13abe493c..1a7fdb7151c79d 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -107,6 +107,7 @@ derivative, differentiable, Fréchet, calculus
 -/
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
+open ContinuousLinearMap (id)
 
 noncomputable section
 
diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean
index 249e086178c811..9eb48ebf4003eb 100644
--- a/Mathlib/Analysis/Normed/Operator/Basic.lean
+++ b/Mathlib/Analysis/Normed/Operator/Basic.lean
@@ -37,7 +37,7 @@ variable {𝕜 𝕜₂ 𝕜₃ E F Fₗ G 𝓕 : Type*}
 
 section SemiNormed
 
-open Metric ContinuousLinearMap
+open Metric
 open ContinuousLinearMap (id)
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup Fₗ]
diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index e16b5094ee9ff0..9d252c90c08031 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -26,7 +26,8 @@ variable {𝕜 𝕜₂ 𝕜₃ E Eₗ F Fₗ G Gₗ 𝓕 : Type*}
 
 section SemiNormed
 
-open Metric ContinuousLinearMap
+open Metric
+open ContinuousLinearMap (id)
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup F]
   [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup G] [SeminormedAddCommGroup Gₗ]

From c8e24b1d4415480f9086ef9a6d5bcfb9b8f12f22 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 12:51:48 +0200
Subject: [PATCH 10/28] fix

---
 Mathlib/Analysis/Normed/Operator/NormedSpace.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
index 8529b0ecb99be5..0101f3b10d0e4a 100644
--- a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
+++ b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
@@ -29,6 +29,7 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G]
   [NormedAddCommGroup Fₗ]
 
 open Metric ContinuousLinearMap
+open ContinuousLinearMap (id)
 
 section
 

From a6a70554f4421da2cac54bed1460c209233087f3 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 13:01:32 +0200
Subject: [PATCH 11/28] fix

---
 Mathlib/Analysis/Calculus/FDeriv/Add.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
index 90cb8899408ce0..9d6cd1103dc9a4 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
@@ -23,6 +23,7 @@ This file contains the usual formulas (and existence assertions) for the derivat
 
 
 open Filter Asymptotics ContinuousLinearMap
+open ContinuousLinearMap (id)
 
 noncomputable section
 

From fc7aade7c3183ffa9bf15ee36d0a55d84d86fa9e Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 13:11:49 +0200
Subject: [PATCH 12/28] fix

---
 Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean b/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
index 079390773bf692..d80f40c6be121f 100644
--- a/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
+++ b/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
@@ -48,7 +48,8 @@ variable {X Y Z : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAd
 
 section LocConformality
 
-open LinearIsometry ContinuousLinearMap
+open LinearIsometry
+open ContinuousLinearMap (id)
 
 /-- A map `f` is said to be conformal if it has a conformal differential `f'`. -/
 def ConformalAt (f : X → Y) (x : X) :=

From 9ba1ed6040485b51d6263df9e4fccad3f2d7ffb9 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 15:29:48 +0200
Subject: [PATCH 13/28] feat: covInnerBilin of the push-forward measure

---
 Mathlib/Probability/Moments/Basic.lean        | 24 +++++++++++++++++++
 .../Probability/Moments/CovInnerBilin.lean    | 14 ++++++++++-
 2 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean
index 3cfd8a1a47fd0f..a2245a700c11a0 100644
--- a/Mathlib/Probability/Moments/Basic.lean
+++ b/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
diff --git a/Mathlib/Probability/Moments/CovInnerBilin.lean b/Mathlib/Probability/Moments/CovInnerBilin.lean
index 996b91305fdef5..c7a8ea609c4d33 100644
--- a/Mathlib/Probability/Moments/CovInnerBilin.lean
+++ b/Mathlib/Probability/Moments/CovInnerBilin.lean
@@ -3,8 +3,9 @@ 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.Dual
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.CovarianceBilin
 
 /-!
@@ -94,6 +95,17 @@ lemma isPosSemidef_covInnerBilin [CompleteSpace E] [IsFiniteMeasure μ] :
   eq := covInnerBilin_comm
   nonneg := covInnerBilin_self_nonneg
 
+lemma covInnerBilin_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) :
+    covInnerBilin (μ.map L) u v = covInnerBilin μ (L.adjoint u) (L.adjoint v) := by
+  rw [covInnerBilin_apply, covInnerBilin_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 covInnerBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] (c : E) :
     covInnerBilin (μ.map (fun x ↦ c + x)) = covInnerBilin μ := by
   by_cases h : MemLp id 2 μ

From 61ae1a9d15e30edf4bb5c31c3ca1a2f509700192 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Thu, 9 Oct 2025 15:30:21 +0200
Subject: [PATCH 14/28] typo in doc

---
 Mathlib/Probability/Moments/CovInnerBilin.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments/CovInnerBilin.lean b/Mathlib/Probability/Moments/CovInnerBilin.lean
index 996b91305fdef5..78fdf0cde0df21 100644
--- a/Mathlib/Probability/Moments/CovInnerBilin.lean
+++ b/Mathlib/Probability/Moments/CovInnerBilin.lean
@@ -16,7 +16,7 @@ bilinear form which maps `L₁ L₂ : StrongDual ℝ E` to `cov[L₁, L₂; μ]`
 
 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 `covInnerBilin`,
-which is bilinear form mapping `x y : E` to `cov[⟪x, ·⟫, ⟪y, ·⟫; μ]`.
+which is a continuous bilinear form mapping `x y : E` to `cov[⟪x, ·⟫, ⟪y, ·⟫; μ]`.
 
 ## Main definition
 

From b2600e48e7441443335170ea3ff86f18d410d954 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Fri, 10 Oct 2025 21:32:38 +0200
Subject: [PATCH 15/28] refactor: rename covarianceBilin to covarianceBilinDual

---
 Mathlib.lean                                  |  2 +-
 ...nceBilin.lean => CovarianceBilinDual.lean} | 84 +++++++++----------
 2 files changed, 43 insertions(+), 43 deletions(-)
 rename Mathlib/Probability/Moments/{CovarianceBilin.lean => CovarianceBilinDual.lean} (72%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 574f3b87bfe3a4..55442fc869a73e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5367,7 +5367,7 @@ import Mathlib.Probability.Martingale.Upcrossing
 import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.ComplexMGF
 import Mathlib.Probability.Moments.Covariance
-import Mathlib.Probability.Moments.CovarianceBilin
+import Mathlib.Probability.Moments.CovarianceBilinDual
 import Mathlib.Probability.Moments.IntegrableExpMul
 import Mathlib.Probability.Moments.MGFAnalytic
 import Mathlib.Probability.Moments.SubGaussian
diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
similarity index 72%
rename from Mathlib/Probability/Moments/CovarianceBilin.lean
rename to Mathlib/Probability/Moments/CovarianceBilinDual.lean
index 4dc3b4dbbb90cc..5ff102ff992fbb 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -20,15 +20,15 @@ Let `μ` be a finite measure on a normed space `E` with the Borel σ-algebra. We
 * `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,
+* `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 `covarianceBilin μ = 0`.
+  If the second moment of `μ` is not finite, we set `covarianceBilinDual μ = 0`.
 
 ## Main statements
 
-* `covarianceBilin_apply` : the covariance of `μ` on `L₁, L₂ : Dual ℝ E` is equal to
+* `covarianceBilinDual_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; μ]`.
+* `covarianceBilinDual_same_eq_variance`: `covarianceBilinDual μ L L = Var[L; μ]`.
 
 ## Implementation notes
 
@@ -162,13 +162,13 @@ variable [NormedSpace ℝ E] [OpensMeasurableSpace E]
 /-- Continuous bilinear form with value `∫ x, L₁ x * L₂ x ∂μ` on `(L₁, L₂)`.
 This is equal to the covariance only if `μ` is centered. -/
 noncomputable
-def uncenteredCovarianceBilin (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
+def uncenteredcovarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
   ContinuousLinearMap.bilinearComp (isBoundedBilinearMap_inner (𝕜 := ℝ)).toContinuousLinearMap
     (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)
 
-lemma uncenteredCovarianceBilin_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    uncenteredCovarianceBilin μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ := by
-  simp only [uncenteredCovarianceBilin, ContinuousLinearMap.bilinearComp_apply,
+lemma uncenteredcovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    uncenteredcovarianceBilinDual μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ := by
+  simp only [uncenteredcovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
     StrongDual.toLp_apply h, L2.inner_def, RCLike.inner_apply, conj_trivial]
   refine integral_congr_ae ?_
   filter_upwards [MemLp.coeFn_toLp (h.continuousLinearMap_comp L₁),
@@ -176,21 +176,21 @@ lemma uncenteredCovarianceBilin_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDua
   simp only [id_eq] at hxL₁ hxL₂
   rw [hxL₁, hxL₂, mul_comm]
 
-lemma uncenteredCovarianceBilin_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    uncenteredCovarianceBilin μ L₁ L₂ = 0 := by
-  simp [uncenteredCovarianceBilin, StrongDual.toLp_of_not_memLp h]
+lemma uncenteredcovarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    uncenteredcovarianceBilinDual μ L₁ L₂ = 0 := by
+  simp [uncenteredcovarianceBilinDual, StrongDual.toLp_of_not_memLp h]
 
-lemma uncenteredCovarianceBilin_zero : uncenteredCovarianceBilin (0 : Measure E) = 0 := by
+lemma uncenteredcovarianceBilinDual_zero : uncenteredcovarianceBilinDual (0 : Measure E) = 0 := by
   ext
   have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
-  simp [uncenteredCovarianceBilin, Subsingleton.eq_zero (StrongDual.toLp 0 2)]
+  simp [uncenteredcovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]
 
-lemma norm_uncenteredCovarianceBilin_le (L₁ L₂ : StrongDual ℝ E) :
-    ‖uncenteredCovarianceBilin μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
+lemma norm_uncenteredcovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
+    ‖uncenteredcovarianceBilinDual μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
   by_cases h : MemLp id 2 μ
-  swap; · simp only [uncenteredCovarianceBilin_of_not_memLp h, norm_zero]; positivity
-  calc ‖uncenteredCovarianceBilin μ L₁ L₂‖
-  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilin_apply h]
+  swap; · simp only [uncenteredcovarianceBilinDual_of_not_memLp h, norm_zero]; positivity
+  calc ‖uncenteredcovarianceBilinDual μ L₁ L₂‖
+  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredcovarianceBilinDual_apply h]
   _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
   _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
     refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
@@ -222,13 +222,13 @@ open Classical in
 /-- 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. -/
 noncomputable
-def covarianceBilin (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
-  uncenteredCovarianceBilin (μ.map (fun x ↦ x - ∫ x, x ∂μ))
+def covarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
+  uncenteredcovarianceBilinDual (μ.map (fun x ↦ x - ∫ x, x ∂μ))
 
 @[simp]
-lemma covarianceBilin_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    covarianceBilin μ L₁ L₂ = 0 := by
-  rw [covarianceBilin, uncenteredCovarianceBilin_of_not_memLp]
+lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = 0 := by
+  rw [covarianceBilinDual, uncenteredcovarianceBilinDual_of_not_memLp]
   rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]
   refine fun h_Lp ↦ h ?_
   have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
@@ -236,45 +236,45 @@ lemma covarianceBilin_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDua
   exact h_Lp.add (memLp_const _)
 
 @[simp]
-lemma covarianceBilin_zero : covarianceBilin (0 : Measure E) = 0 := by
-  rw [covarianceBilin, Measure.map_zero, uncenteredCovarianceBilin_zero]
+lemma covarianceBilinDual_zero : covarianceBilinDual (0 : Measure E) = 0 := by
+  rw [covarianceBilinDual, Measure.map_zero, uncenteredcovarianceBilinDual_zero]
 
-lemma covarianceBilin_comm (L₁ L₂ : StrongDual ℝ E) :
-    covarianceBilin μ L₁ L₂ = covarianceBilin μ L₂ L₁ := by
+lemma covarianceBilinDual_comm (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = covarianceBilinDual μ L₂ L₁ := by
   by_cases h : MemLp id 2 μ
   · have h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) :=
       (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)
-    simp_rw [covarianceBilin, uncenteredCovarianceBilin_apply h', mul_comm (L₁ _)]
+    simp_rw [covarianceBilinDual, uncenteredcovarianceBilinDual_apply h', mul_comm (L₁ _)]
   · simp [h]
 
 variable [CompleteSpace E]
 
-lemma covarianceBilin_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    covarianceBilin μ L₁ L₂ = ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ := by
-  rw [covarianceBilin, uncenteredCovarianceBilin_apply,
+lemma covarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ := by
+  rw [covarianceBilinDual, uncenteredcovarianceBilinDual_apply,
     integral_map (by fun_prop) (by fun_prop)]
   · have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
       L.integral_comp_comm (h.integrable (by simp))
     simp [← hL]
   · exact (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)
 
-lemma covarianceBilin_apply' (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    covarianceBilin μ L₁ L₂ = ∫ x, L₁ (x - μ[id]) * L₂ (x - μ[id]) ∂μ := by
-  rw [covarianceBilin_apply h]
+lemma covarianceBilinDual_apply' (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = ∫ x, L₁ (x - μ[id]) * L₂ (x - μ[id]) ∂μ := by
+  rw [covarianceBilinDual_apply h]
   have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
     L.integral_comp_comm (h.integrable (by simp))
   simp [← hL]
 
-lemma covarianceBilin_eq_covariance (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    covarianceBilin μ L₁ L₂ = cov[L₁, L₂; μ] := by
-  rw [covarianceBilin_apply h, covariance]
+lemma covarianceBilinDual_eq_covariance (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = cov[L₁, L₂; μ] := by
+  rw [covarianceBilinDual_apply h, covariance]
 
-lemma covarianceBilin_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual ℝ E) :
-    covarianceBilin μ L L = Var[L; μ] := by
-  rw [covarianceBilin_eq_covariance h, covariance_self (by fun_prop)]
+lemma covarianceBilinDual_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual ℝ E) :
+    covarianceBilinDual μ L L = Var[L; μ] := by
+  rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]
 
-@[deprecated (since := "2025-07-16")] alias covarianceBilin_same_eq_variance :=
-  covarianceBilin_self_eq_variance
+@[deprecated (since := "2025-07-16")] alias covarianceBilinDual_same_eq_variance :=
+  covarianceBilinDual_self_eq_variance
 
 end Covariance
 

From e4adcbde245277edae61694044c7dfa9c28d2a3b Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Fri, 10 Oct 2025 21:34:58 +0200
Subject: [PATCH 16/28] fix

---
 Mathlib/Probability/Moments/CovarianceBilinDual.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
index 5ff102ff992fbb..502e50018a70b3 100644
--- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -273,7 +273,7 @@ lemma covarianceBilinDual_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual 
     covarianceBilinDual μ L L = Var[L; μ] := by
   rw [covarianceBilinDual_eq_covariance h, covariance_self (by fun_prop)]
 
-@[deprecated (since := "2025-07-16")] alias covarianceBilinDual_same_eq_variance :=
+@[deprecated (since := "2025-07-16")] alias covarianceBilin_same_eq_variance :=
   covarianceBilinDual_self_eq_variance
 
 end Covariance

From 636875dd488b5358581e3a216bd0a2c136d15514 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Fri, 10 Oct 2025 21:39:06 +0200
Subject: [PATCH 17/28] deprecations

---
 .../Probability/Moments/CovarianceBilinDual.lean  | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
index 502e50018a70b3..bb9bbf7693783c 100644
--- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -166,6 +166,9 @@ def uncenteredcovarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ]
   ContinuousLinearMap.bilinearComp (isBoundedBilinearMap_inner (𝕜 := ℝ)).toContinuousLinearMap
     (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)
 
+@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin :=
+  uncenteredcovarianceBilinDual
+
 lemma uncenteredcovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
     uncenteredcovarianceBilinDual μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ := by
   simp only [uncenteredcovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
@@ -176,15 +179,24 @@ lemma uncenteredcovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : Stron
   simp only [id_eq] at hxL₁ hxL₂
   rw [hxL₁, hxL₂, mul_comm]
 
+@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_apply :=
+  uncenteredcovarianceBilinDual_apply
+
 lemma uncenteredcovarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
     uncenteredcovarianceBilinDual μ L₁ L₂ = 0 := by
   simp [uncenteredcovarianceBilinDual, StrongDual.toLp_of_not_memLp h]
 
+@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_of_not_memLp :=
+  uncenteredcovarianceBilinDual_of_not_memLp
+
 lemma uncenteredcovarianceBilinDual_zero : uncenteredcovarianceBilinDual (0 : Measure E) = 0 := by
   ext
   have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
   simp [uncenteredcovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]
 
+@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_zero :=
+  uncenteredcovarianceBilinDual_zero
+
 lemma norm_uncenteredcovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
     ‖uncenteredcovarianceBilinDual μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
   by_cases h : MemLp id 2 μ
@@ -212,6 +224,9 @@ lemma norm_uncenteredcovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
     congr with x
     ring
 
+@[deprecated (since := "2025-10-10")] alias norm_uncenteredcovarianceBilin_le :=
+  norm_uncenteredcovarianceBilinDual_le
+
 end Centered
 
 section Covariance

From 140742fc52b2af1450e0f115f1b3931435c99f04 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Fri, 10 Oct 2025 21:58:35 +0200
Subject: [PATCH 18/28] fix

---
 Mathlib.lean                                                    | 2 +-
 .../Moments/{CovInnerBilin.lean => CovarianceBilin.lean}        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)
 rename Mathlib/Probability/Moments/{CovInnerBilin.lean => CovarianceBilin.lean} (99%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 7692e5675ef70f..4a653b61ffb014 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5366,8 +5366,8 @@ import Mathlib.Probability.Martingale.OptionalStopping
 import Mathlib.Probability.Martingale.Upcrossing
 import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.ComplexMGF
-import Mathlib.Probability.Moments.CovInnerBilin
 import Mathlib.Probability.Moments.Covariance
+import Mathlib.Probability.Moments.CovarianceBilin
 import Mathlib.Probability.Moments.CovarianceBilinDual
 import Mathlib.Probability.Moments.IntegrableExpMul
 import Mathlib.Probability.Moments.MGFAnalytic
diff --git a/Mathlib/Probability/Moments/CovInnerBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
similarity index 99%
rename from Mathlib/Probability/Moments/CovInnerBilin.lean
rename to Mathlib/Probability/Moments/CovarianceBilin.lean
index 78fdf0cde0df21..a9cd39f3cb190f 100644
--- a/Mathlib/Probability/Moments/CovInnerBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -5,7 +5,7 @@ Authors: Rémy Degenne, Etienne Marion
 -/
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.MeasureTheory.SpecificCodomains.WithLp
-import Mathlib.Probability.Moments.CovarianceBilin
+import Mathlib.Probability.Moments.CovarianceBilinDual
 
 /-!
 # Covariance in Hilbert spaces

From 0322c9650bb1e4ba8d78e5db6585ca7d05966b55 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Sun, 12 Oct 2025 19:30:59 +0200
Subject: [PATCH 19/28] fix naming

---
 .../Moments/CovarianceBilinDual.lean          | 58 +++++++++----------
 1 file changed, 29 insertions(+), 29 deletions(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
index bb9bbf7693783c..ad5aa16684f49d 100644
--- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -162,16 +162,16 @@ variable [NormedSpace ℝ E] [OpensMeasurableSpace E]
 /-- Continuous bilinear form with value `∫ x, L₁ x * L₂ x ∂μ` on `(L₁, L₂)`.
 This is equal to the covariance only if `μ` is centered. -/
 noncomputable
-def uncenteredcovarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
+def uncenteredCovarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
   ContinuousLinearMap.bilinearComp (isBoundedBilinearMap_inner (𝕜 := ℝ)).toContinuousLinearMap
     (StrongDual.toLp μ 2) (StrongDual.toLp μ 2)
 
-@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin :=
-  uncenteredcovarianceBilinDual
+@[deprecated (since := "2025-10-10")] alias uncenteredCovarianceBilin :=
+  uncenteredCovarianceBilinDual
 
-lemma uncenteredcovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    uncenteredcovarianceBilinDual μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ := by
-  simp only [uncenteredcovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
+lemma uncenteredCovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    uncenteredCovarianceBilinDual μ L₁ L₂ = ∫ x, L₁ x * L₂ x ∂μ := by
+  simp only [uncenteredCovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
     StrongDual.toLp_apply h, L2.inner_def, RCLike.inner_apply, conj_trivial]
   refine integral_congr_ae ?_
   filter_upwards [MemLp.coeFn_toLp (h.continuousLinearMap_comp L₁),
@@ -179,30 +179,30 @@ lemma uncenteredcovarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : Stron
   simp only [id_eq] at hxL₁ hxL₂
   rw [hxL₁, hxL₂, mul_comm]
 
-@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_apply :=
-  uncenteredcovarianceBilinDual_apply
+@[deprecated (since := "2025-10-10")] alias uncenteredCovarianceBilin_apply :=
+  uncenteredCovarianceBilinDual_apply
 
-lemma uncenteredcovarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
-    uncenteredcovarianceBilinDual μ L₁ L₂ = 0 := by
-  simp [uncenteredcovarianceBilinDual, StrongDual.toLp_of_not_memLp h]
+lemma uncenteredCovarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    uncenteredCovarianceBilinDual μ L₁ L₂ = 0 := by
+  simp [uncenteredCovarianceBilinDual, StrongDual.toLp_of_not_memLp h]
 
-@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_of_not_memLp :=
-  uncenteredcovarianceBilinDual_of_not_memLp
+@[deprecated (since := "2025-10-10")] alias uncenteredCovarianceBilin_of_not_memLp :=
+  uncenteredCovarianceBilinDual_of_not_memLp
 
-lemma uncenteredcovarianceBilinDual_zero : uncenteredcovarianceBilinDual (0 : Measure E) = 0 := by
+lemma uncenteredCovarianceBilinDual_zero : uncenteredCovarianceBilinDual (0 : Measure E) = 0 := by
   ext
   have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩
-  simp [uncenteredcovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]
+  simp [uncenteredCovarianceBilinDual, Subsingleton.eq_zero (StrongDual.toLp 0 2)]
 
-@[deprecated (since := "2025-10-10")] alias uncenteredcovarianceBilin_zero :=
-  uncenteredcovarianceBilinDual_zero
+@[deprecated (since := "2025-10-10")] alias uncenteredCovarianceBilin_zero :=
+  uncenteredCovarianceBilinDual_zero
 
-lemma norm_uncenteredcovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
-    ‖uncenteredcovarianceBilinDual μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
+lemma norm_uncenteredCovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
+    ‖uncenteredCovarianceBilinDual μ L₁ L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ x, ‖x‖ ^ 2 ∂μ := by
   by_cases h : MemLp id 2 μ
-  swap; · simp only [uncenteredcovarianceBilinDual_of_not_memLp h, norm_zero]; positivity
-  calc ‖uncenteredcovarianceBilinDual μ L₁ L₂‖
-  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredcovarianceBilinDual_apply h]
+  swap; · simp only [uncenteredCovarianceBilinDual_of_not_memLp h, norm_zero]; positivity
+  calc ‖uncenteredCovarianceBilinDual μ L₁ L₂‖
+  _ = ‖∫ x, L₁ x * L₂ x ∂μ‖ := by rw [uncenteredCovarianceBilinDual_apply h]
   _ ≤ ∫ x, ‖L₁ x‖ * ‖L₂ x‖ ∂μ := (norm_integral_le_integral_norm _).trans (by simp)
   _ ≤ ∫ x, ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖ ∂μ := by
     refine integral_mono_ae ?_ ?_ (ae_of_all _ fun x ↦ ?_)
@@ -224,8 +224,8 @@ lemma norm_uncenteredcovarianceBilinDual_le (L₁ L₂ : StrongDual ℝ E) :
     congr with x
     ring
 
-@[deprecated (since := "2025-10-10")] alias norm_uncenteredcovarianceBilin_le :=
-  norm_uncenteredcovarianceBilinDual_le
+@[deprecated (since := "2025-10-10")] alias norm_uncenteredCovarianceBilin_le :=
+  norm_uncenteredCovarianceBilinDual_le
 
 end Centered
 
@@ -238,12 +238,12 @@ open Classical in
 if `MemLp id 2 μ`. If not, we set it to zero. -/
 noncomputable
 def covarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
-  uncenteredcovarianceBilinDual (μ.map (fun x ↦ x - ∫ x, x ∂μ))
+  uncenteredCovarianceBilinDual (μ.map (fun x ↦ x - ∫ x, x ∂μ))
 
 @[simp]
 lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
     covarianceBilinDual μ L₁ L₂ = 0 := by
-  rw [covarianceBilinDual, uncenteredcovarianceBilinDual_of_not_memLp]
+  rw [covarianceBilinDual, uncenteredCovarianceBilinDual_of_not_memLp]
   rw [(measurableEmbedding_subRight _).memLp_map_measure_iff]
   refine fun h_Lp ↦ h ?_
   have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
@@ -252,21 +252,21 @@ lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : Stron
 
 @[simp]
 lemma covarianceBilinDual_zero : covarianceBilinDual (0 : Measure E) = 0 := by
-  rw [covarianceBilinDual, Measure.map_zero, uncenteredcovarianceBilinDual_zero]
+  rw [covarianceBilinDual, Measure.map_zero, uncenteredCovarianceBilinDual_zero]
 
 lemma covarianceBilinDual_comm (L₁ L₂ : StrongDual ℝ E) :
     covarianceBilinDual μ L₁ L₂ = covarianceBilinDual μ L₂ L₁ := by
   by_cases h : MemLp id 2 μ
   · have h' : MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ) :=
       (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h.sub (memLp_const _)
-    simp_rw [covarianceBilinDual, uncenteredcovarianceBilinDual_apply h', mul_comm (L₁ _)]
+    simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]
   · simp [h]
 
 variable [CompleteSpace E]
 
 lemma covarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
     covarianceBilinDual μ L₁ L₂ = ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ := by
-  rw [covarianceBilinDual, uncenteredcovarianceBilinDual_apply,
+  rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply,
     integral_map (by fun_prop) (by fun_prop)]
   · have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
       L.integral_comp_comm (h.integrable (by simp))

From a78c6048acd69e7a523aa970108cc12f81f86972 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Sun, 12 Oct 2025 19:35:44 +0200
Subject: [PATCH 20/28] fix

---
 .../Probability/Moments/CovarianceBilin.lean  | 105 +++++++++---------
 1 file changed, 54 insertions(+), 51 deletions(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index a9cd39f3cb190f..98a5b7702f3c39 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -12,15 +12,16 @@ import Mathlib.Probability.Moments.CovarianceBilinDual
 
 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
-`CovarianceBilin μ` and is defined in the `CovarianceBilin` file.
+`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 `covInnerBilin`,
-which is a continuous bilinear form mapping `x y : E` to `cov[⟪x, ·⟫, ⟪y, ·⟫; μ]`.
+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
 
-* `covInnerBilin μ`: the continuous bilinear form over `E` representing the covariance of a
+* `covarianceBilin μ`: the continuous bilinear form over `E` representing the covariance of a
   measure over `E`.
 
 ## Tags
@@ -37,70 +38,72 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
 /-- Covariance of a measure on an inner product space, as a continuous bilinear form. -/
 noncomputable
-def covInnerBilin (μ : Measure E) : E →L[ℝ] E →L[ℝ] ℝ :=
-  ContinuousLinearMap.bilinearComp (covarianceBilin μ)
+def covarianceBilin (μ : Measure E) : E →L[ℝ] E →L[ℝ] ℝ :=
+  ContinuousLinearMap.bilinearComp (covarianceBilinDual μ)
     (toDualMap ℝ E).toContinuousLinearMap (toDualMap ℝ E).toContinuousLinearMap
 
 @[simp]
-lemma covInnerBilin_zero : covInnerBilin (0 : Measure E) = 0 := by
-  rw [covInnerBilin]
+lemma covarianceBilin_zero : covarianceBilin (0 : Measure E) = 0 := by
+  rw [covarianceBilin]
   simp
 
-lemma covInnerBilin_eq_covarianceBilin (x y : E) :
-    covInnerBilin μ x y = covarianceBilin μ (toDualMap ℝ E x) (toDualMap ℝ E y) := rfl
+lemma covarianceBilin_eq_covarianceBilinDual (x y : E) :
+    covarianceBilin μ x y = covarianceBilinDual μ (toDualMap ℝ E x) (toDualMap ℝ E y) := rfl
 
 @[simp]
-lemma covInnerBilin_of_not_memLp [IsFiniteMeasure μ] (h : ¬MemLp id 2 μ) :
-    covInnerBilin μ = 0 := by
+lemma covarianceBilin_of_not_memLp [IsFiniteMeasure μ] (h : ¬MemLp id 2 μ) :
+    covarianceBilin μ = 0 := by
   ext
-  simp [covInnerBilin_eq_covarianceBilin, h]
+  simp [covarianceBilin_eq_covarianceBilinDual, h]
 
-lemma covInnerBilin_apply [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
-    covInnerBilin μ x y = ∫ z, ⟪x, z - μ[id]⟫_ℝ * ⟪y, z - μ[id]⟫_ℝ ∂μ := by
-  simp_rw [covInnerBilin, ContinuousLinearMap.bilinearComp_apply, covarianceBilin_apply' 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 covInnerBilin_comm [IsFiniteMeasure μ] (x y : E) :
-    covInnerBilin μ x y = covInnerBilin μ y x := by
-  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_comm, covInnerBilin_eq_covarianceBilin]
+lemma covarianceBilin_comm [IsFiniteMeasure μ] (x y : E) :
+    covarianceBilin μ x y = covarianceBilin μ y x := by
+  rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
+    covarianceBilin_eq_covarianceBilinDual]
 
-lemma covInnerBilin_self [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : E) :
-    covInnerBilin μ x x = Var[fun u ↦ ⟪x, u⟫_ℝ; μ] := by
-  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_self_eq_variance h]
+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 covInnerBilin_apply_eq [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
-    covInnerBilin μ x y = cov[fun u ↦ ⟪x, u⟫_ℝ, fun u ↦ ⟪y, u⟫_ℝ; μ] := by
-  rw [covInnerBilin_eq_covarianceBilin, covarianceBilin_eq_covariance h]
+lemma covarianceBilin_apply_eq [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 covInnerBilin_real {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : ℝ) :
-    covInnerBilin μ x y = x * y * Var[id; μ] := by
-  simp only [covInnerBilin_apply_eq h, RCLike.inner_apply, conj_trivial, mul_comm]
+lemma covarianceBilin_real {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : ℝ) :
+    covarianceBilin μ x y = x * y * Var[id; μ] := by
+  simp only [covarianceBilin_apply_eq h, RCLike.inner_apply, conj_trivial, mul_comm]
   rw [covariance_mul_left, covariance_mul_right, ← mul_assoc, covariance_self aemeasurable_id']
   rfl
 
-lemma covInnerBilin_real_self {μ : Measure ℝ} [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x : ℝ) :
-    covInnerBilin μ x x = x ^ 2 * Var[id; μ] := by
-  rw [covInnerBilin_real h, pow_two]
+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 covInnerBilin_self_nonneg [CompleteSpace E] [IsFiniteMeasure μ] (x : E) :
-    0 ≤ covInnerBilin μ x x := by
-  simp [covInnerBilin]
+lemma covarianceBilin_self_nonneg [CompleteSpace E] [IsFiniteMeasure μ] (x : E) :
+    0 ≤ covarianceBilin μ x x := by
+  simp [covarianceBilin]
 
-lemma isPosSemidef_covInnerBilin [CompleteSpace E] [IsFiniteMeasure μ] :
-    (covInnerBilin μ).toBilinForm.IsPosSemidef where
-  eq := covInnerBilin_comm
-  nonneg := covInnerBilin_self_nonneg
+lemma isPosSemidef_covarianceBilin [CompleteSpace E] [IsFiniteMeasure μ] :
+    (covarianceBilin μ).toBilinForm.IsPosSemidef where
+  eq := covarianceBilin_comm
+  nonneg := covarianceBilin_self_nonneg
 
-lemma covInnerBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] (c : E) :
-    covInnerBilin (μ.map (fun x ↦ c + x)) = covInnerBilin μ := by
+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 [covInnerBilin_apply h_Lp, covInnerBilin_apply h, integral_map (by fun_prop) (by fun_prop)]
+    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]
@@ -108,39 +111,39 @@ lemma covInnerBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] (c
     · simp
     · exact h.integrable (by simp)
   · ext
-    rw [covInnerBilin_of_not_memLp, covInnerBilin_of_not_memLp h]
+    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 covInnerBilin_apply_basisFun {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+lemma covarianceBilin_apply_basisFun {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
     {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i j : ι) :
-    covInnerBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+    covarianceBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
       (basisFun ι ℝ i) (basisFun ι ℝ j) = cov[X i, X j; μ] := by
   have (i : ι) := (hX i).aemeasurable
-  rw [covInnerBilin_apply_eq, covariance_map]
+  rw [covarianceBilin_apply_eq, 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 covInnerBilin_apply_basisFun_self {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+lemma covarianceBilin_apply_basisFun_self {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
     {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (hX : ∀ i, MemLp (X i) 2 μ) (i : ι) :
-    covInnerBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
+    covarianceBilin (μ.map (fun ω ↦ toLp 2 (X · ω)))
       (basisFun ι ℝ i) (basisFun ι ℝ i) = Var[X i; μ] := by
-  rw [covInnerBilin_apply_basisFun hX, covariance_self]
+  rw [covarianceBilin_apply_basisFun hX, covariance_self]
   have (i : ι) := (hX i).aemeasurable
   fun_prop
 
-lemma covInnerBilin_apply_pi {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
+lemma covarianceBilin_apply_pi {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω}
     {μ : Measure Ω} [IsFiniteMeasure μ] {X : ι → Ω → ℝ}
     (hX : ∀ i, MemLp (X i) 2 μ) (x y : EuclideanSpace ℝ ι) :
-    covInnerBilin (μ.map (fun ω ↦ toLp 2 (X · ω))) x y =
+    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 [covInnerBilin_apply_eq, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
+  nth_rw 1 [covarianceBilin_apply_eq, 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]

From b6e8803f95db9cc69a825d0341ed949dc36341a7 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 13:44:56 +0200
Subject: [PATCH 21/28] merge

---
 .../Probability/Moments/CovarianceBilin.lean  | 158 ++++++++++++++++++
 1 file changed, 158 insertions(+)
 create mode 100644 Mathlib/Probability/Moments/CovarianceBilin.lean

diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
new file mode 100644
index 00000000000000..98a5b7702f3c39
--- /dev/null
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -0,0 +1,158 @@
+/-
+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.Dual
+import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.CovarianceBilinDual
+
+/-!
+# 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 [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 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_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, 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, 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

From 31ce54faf2940f9f79a4064e2f92382af4720139 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 14:23:36 +0200
Subject: [PATCH 22/28] fix

---
 Mathlib/Probability/Moments/CovarianceBilinDual.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
index ad5aa16684f49d..e1fc4b9097f8e3 100644
--- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -291,6 +291,14 @@ 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

From da839ec146220518f8f80eecd47b72af846d896e Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 14:24:01 +0200
Subject: [PATCH 23/28] alignment

---
 Mathlib/Probability/Moments/CovarianceBilinDual.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
index e1fc4b9097f8e3..65ee2770b1925d 100644
--- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean
@@ -292,8 +292,7 @@ lemma covarianceBilinDual_self_eq_variance (h : MemLp id 2 μ) (L : StrongDual 
   covarianceBilinDual_self_eq_variance
 
 @[simp]
-lemma covarianceBilinDual_self_nonneg (L : StrongDual ℝ E) :
-    0 ≤ covarianceBilinDual μ L L := by
+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 ..

From 2d51947114b0574db41474fdea08b31c1e062f28 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 15:32:55 +0200
Subject: [PATCH 24/28] update

---
 Mathlib/Probability/Moments/CovarianceBilin.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index 98a5b7702f3c39..6e5a4bbe0cd549 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -96,6 +96,17 @@ lemma isPosSemidef_covarianceBilin [CompleteSpace E] [IsFiniteMeasure μ] :
   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 μ

From 37e0159dcb863e45a6c4d70c1ea4d763b4598b67 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 16:35:32 +0200
Subject: [PATCH 25/28] better name

---
 Mathlib/Probability/Moments/CovarianceBilin.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index 98a5b7702f3c39..b157e1af88d00f 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -71,14 +71,15 @@ lemma covarianceBilin_self [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id
   rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_self_eq_variance h]
   rfl
 
-lemma covarianceBilin_apply_eq [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id 2 μ) (x y : E) :
+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 h, RCLike.inner_apply, conj_trivial, mul_comm]
+  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
 
@@ -122,7 +123,7 @@ lemma covarianceBilin_apply_basisFun {ι Ω : Type*} [Fintype ι] {mΩ : Measura
     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, covariance_map]
+  rw [covarianceBilin_apply_eq_cov, covariance_map]
   · simp [basisFun_inner]; rfl
   · exact Measurable.aestronglyMeasurable (by fun_prop)
   · exact Measurable.aestronglyMeasurable (by fun_prop)
@@ -143,7 +144,7 @@ lemma covarianceBilin_apply_pi {ι Ω : Type*} [Fintype ι] {mΩ : MeasurableSpa
     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, covariance_map_fun, ← (basisFun ι ℝ).sum_repr' x,
+  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]

From 71483ccbc9795c9eedfbde33dce9088ed468499a Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 17:39:52 +0200
Subject: [PATCH 26/28] fix merge

---
 Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean | 3 +--
 Mathlib/Topology/Algebra/Module/LinearMap.lean       | 4 ----
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean b/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
index 80e05cf8105c1f..fdb955faa223e9 100644
--- a/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
+++ b/Mathlib/Analysis/Calculus/Conformal/NormedSpace.lean
@@ -48,8 +48,7 @@ variable {X Y Z : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAd
 
 section LocConformality
 
-open LinearIsometry
-open ContinuousLinearMap (id)
+open LinearIsometry ContinuousLinearMap
 
 /-- A map `f` is said to be conformal if it has a conformal differential `f'`. -/
 def ConformalAt (f : X → Y) (x : X) :=
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index 7583e2ddb08f3d..df63c647916820 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -318,8 +318,6 @@ protected def id : M₁ →L[R₁] M₁ :=
 
 end
 
-open ContinuousLinearMap (id)
-
 instance one : One (M₁ →L[R₁] M₁) :=
   ⟨.id R₁ M₁⟩
 
@@ -1127,8 +1125,6 @@ end RestrictScalars
 
 end ContinuousLinearMap
 
-open ContinuousLinearMap (id)
-
 namespace Submodule
 
 variable {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]

From 3f0d8617527d9eca0e9c76f1107519303238b3f9 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Mon, 13 Oct 2025 17:44:11 +0200
Subject: [PATCH 27/28] fix merge

---
 Mathlib/Analysis/Calculus/FDeriv/Add.lean            | 1 -
 Mathlib/Analysis/Calculus/FDeriv/Basic.lean          | 1 -
 Mathlib/Analysis/Normed/Operator/Basic.lean          | 3 +--
 Mathlib/Analysis/Normed/Operator/Bilinear.lean       | 3 +--
 Mathlib/Analysis/Normed/Operator/NormedSpace.lean    | 1 -
 Mathlib/Topology/Algebra/Module/Equiv.lean           | 2 --
 Mathlib/Topology/Algebra/Module/LinearMap.lean       | 2 --
 Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean | 1 -
 8 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
index b8e361098c66f6..4dcbdabd2be6f1 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
@@ -23,7 +23,6 @@ This file contains the usual formulas (and existence assertions) for the derivat
 
 
 open Filter Asymptotics ContinuousLinearMap
-open ContinuousLinearMap (id)
 
 noncomputable section
 
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
index 116b8e9f282903..c9dd713ba9422c 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean
@@ -107,7 +107,6 @@ derivative, differentiable, Fréchet, calculus
 -/
 
 open Filter Asymptotics ContinuousLinearMap Set Metric Topology NNReal ENNReal
-open ContinuousLinearMap (id)
 
 noncomputable section
 
diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean
index fd19cb8b481d0b..88079aed1c1c25 100644
--- a/Mathlib/Analysis/Normed/Operator/Basic.lean
+++ b/Mathlib/Analysis/Normed/Operator/Basic.lean
@@ -37,8 +37,7 @@ variable {𝕜 𝕜₂ 𝕜₃ E F Fₗ G 𝓕 : Type*}
 
 section SemiNormed
 
-open Metric
-open ContinuousLinearMap (id)
+open Metric ContinuousLinearMap
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup Fₗ]
   [SeminormedAddCommGroup G]
diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index ec129a379ef28d..51b4e6ffc7f581 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -26,8 +26,7 @@ variable {𝕜 𝕜₂ 𝕜₃ E Eₗ F Fₗ G Gₗ 𝓕 : Type*}
 
 section SemiNormed
 
-open Metric
-open ContinuousLinearMap (id)
+open Metric ContinuousLinearMap
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup F]
   [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup G] [SeminormedAddCommGroup Gₗ]
diff --git a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
index d326cb724b331e..0d8934950cc082 100644
--- a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
+++ b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
@@ -29,7 +29,6 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G]
   [NormedAddCommGroup Fₗ]
 
 open Metric ContinuousLinearMap
-open ContinuousLinearMap (id)
 
 section
 
diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean
index 4756ce99d39263..4deee66c2b848c 100644
--- a/Mathlib/Topology/Algebra/Module/Equiv.lean
+++ b/Mathlib/Topology/Algebra/Module/Equiv.lean
@@ -1028,8 +1028,6 @@ end ContinuousLinearEquiv
 
 namespace ContinuousLinearMap
 
-open ContinuousLinearMap (id)
-
 variable {R : Type*} {M M₂ M₃ : Type*}
   [TopologicalSpace M] [TopologicalSpace M₂] [TopologicalSpace M₃]
 
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index df63c647916820..a213d1bbefcf94 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -757,8 +757,6 @@ end ToSpanSingleton
 
 end Semiring
 
-open ContinuousLinearMap (id)
-
 section Ring
 
 variable {R : Type*} [Ring R] {R₂ : Type*} [Ring R₂] {R₃ : Type*} [Ring R₃] {M : Type*}
diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
index 7cf19407fe85e2..ec6cd56fbcb457 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
@@ -14,7 +14,6 @@ assert_not_exists TrivialStar
 
 open LinearMap (ker range)
 open Topology Filter Pointwise
-open ContinuousLinearMap (id)
 
 universe u v w u'
 

From d5bd14ea61d0f731af0cda0640651c1811cb1814 Mon Sep 17 00:00:00 2001
From: Etienne Marion <baguettes_casino0c@icloud.com>
Date: Tue, 14 Oct 2025 12:36:12 +0200
Subject: [PATCH 28/28] fix

---
 Mathlib/Probability/Moments/CovarianceBilin.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index b6c7ab97c4e1f7..b6e7108e268858 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -3,8 +3,9 @@ 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.Dual
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.CovarianceBilinDual
 
 /-!