diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean
index 485f4acd5a55e0..ace4b0ebdcfa0a 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/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean
index 5b5e26efe497a0..952124e5916dd8 100644
--- a/Mathlib/Probability/Moments/CovarianceBilin.lean
+++ b/Mathlib/Probability/Moments/CovarianceBilin.lean
@@ -3,8 +3,10 @@ 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.Positive
 import Mathlib.MeasureTheory.SpecificCodomains.WithLp
+import Mathlib.Probability.Moments.Basic
 import Mathlib.Probability.Moments.CovarianceBilinDual
 
 /-!
@@ -102,6 +104,17 @@ lemma isPosSemidef_covarianceBilin [IsFiniteMeasure μ] :
   eq := covarianceBilin_comm
   nonneg := covarianceBilin_self_nonneg
 
+lemma covarianceBilin_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+    [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [CompleteSpace F]
+    [CompleteSpace E] [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 μ