feat: drop a finiteness assumptions in covariance results (#31569)

Co-authored-by: Etienne Marion <baguettes_casino0c@icloud.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Rémy Degenne <4094732+RemyDegenne@users.noreply.github.com>

Author: 3 people

Mathlib/Probability/Moments/CovarianceBilin.lean

@@ -56,7 +56,7 @@ 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 μ) :
+lemma covarianceBilin_of_not_memLp (h : ¬MemLp id 2 μ) :
     covarianceBilin μ = 0 := by
   ext
   simp [covarianceBilin_eq_covarianceBilinDual, h]
@@ -66,7 +66,7 @@ lemma covarianceBilin_apply [CompleteSpace E] [IsFiniteMeasure μ] (h : MemLp id
   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) :
+lemma covarianceBilin_comm (x y : E) :
     covarianceBilin μ x y = covarianceBilin μ y x := by
   rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_comm,
     covarianceBilin_eq_covarianceBilinDual]
@@ -95,11 +95,11 @@ lemma covarianceBilin_real_self {μ : Measure ℝ} [IsFiniteMeasure μ] (x : ℝ
   rw [covarianceBilin_real, pow_two]
 
 @[simp]
-lemma covarianceBilin_self_nonneg [IsFiniteMeasure μ] (x : E) :
+lemma covarianceBilin_self_nonneg (x : E) :
     0 ≤ covarianceBilin μ x x := by
   simp [covarianceBilin]
 
-lemma isPosSemidef_covarianceBilin [IsFiniteMeasure μ] :
+lemma isPosSemidef_covarianceBilin :
     (covarianceBilin μ).toBilinForm.IsPosSemidef where
   eq := covarianceBilin_comm
   nonneg := covarianceBilin_self_nonneg

Mathlib/Probability/Moments/CovarianceBilinDual.lean

@@ -232,7 +232,7 @@ end Centered
 
 section Covariance
 
-variable [NormedSpace ℝ E] [BorelSpace E] [IsFiniteMeasure μ]
+variable [NormedSpace ℝ E] [BorelSpace E]
 
 open Classical in
 /-- Continuous bilinear form with value `∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ` on `(L₁, L₂)`
@@ -241,27 +241,80 @@ noncomputable
 def covarianceBilinDual (μ : Measure E) : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
   uncenteredCovarianceBilinDual (μ.map (fun x ↦ x - ∫ x, x ∂μ))
 
-@[simp]
-lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+omit [BorelSpace E] in
+lemma _root_.MeasureTheory.memLp_id_of_self_sub_integral {p : ℝ≥0∞}
+    (h_Lp : MemLp (fun x ↦ x - ∫ y, y ∂μ) p μ) : MemLp id p μ := by
+  have : (id : E → E) = fun x ↦ x - ∫ x, x ∂μ + ∫ x, x ∂μ := by ext; simp
+  rw [this]
+  apply h_Lp.add
+  set c := ∫ x, x ∂μ
+  /- We need to check that the constant `c = ∫ x, x ∂μ` is in `L^p`. Note that we don't assume
+  that `μ` is finite, so this requires an argument. If the constant is zero, it's obvious.
+  If it's nonzero, this means that `x` is integrable for `μ` (as otherwise the integral would be
+  `0` by our choice of junk value), so `‖x‖ ^ (1/p)` is in `L^p`.
+  The constant `c` is controlled by `2 ‖x - c‖` close to `0` (say when `‖x‖ ≤ ‖c‖ / 2`)
+  and by a multiple of `‖x‖ ^ (1/p)` away from `0`. Those two functions
+  are in `L^p` by assumptions, so the constant `c` also is. -/
+  by_cases hx : c = 0
+  · simp [hx]
+  rcases eq_or_ne p 0 with rfl | hp0
+  · simp [aestronglyMeasurable_const]
+  rcases eq_or_ne p ∞ with rfl | hptop
+  · exact memLp_top_const c
+  apply (integrable_norm_rpow_iff (by fun_prop) hp0 hptop).1
+  have I : Integrable (fun (x : E) ↦ ‖x‖) μ := by
+    apply Integrable.norm
+    contrapose! hx
+    exact integral_undef hx
+  have := (h_Lp.integrable_norm_rpow hp0 hptop).const_mul (2 ^ p.toReal)
+  apply (((I.const_mul (2 * ‖c‖ ^ (p.toReal - 1))).add this)).mono' (by fun_prop)
+  filter_upwards [] with y
+  lift p to ℝ≥0 using hptop
+  simp only [ENNReal.coe_toReal, Real.norm_eq_abs, Pi.add_apply]
+  rw [abs_of_nonneg (by positivity)]
+  rcases le_total ‖y‖ (‖c‖ / 2)
+  · have : ‖c‖ ≤ ‖y‖ + ‖y - c‖ := Eq.trans_le (by abel_nf) (norm_sub_le y (y - c))
+    calc ‖c‖ ^ (p : ℝ)
+    _ ≤ (2 * ‖y - c‖) ^ (p : ℝ) :=
+      Real.rpow_le_rpow (by positivity) (by linarith) (by positivity)
+    _ = 0 + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
+      rw [Real.mul_rpow (by simp) (by positivity)]
+      ring
+    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by
+      gcongr
+      positivity
+  · calc ‖c‖ ^ (p : ℝ )
+    _ = ‖c‖ ^ ((p - 1) + 1 : ℝ) := by abel_nf
+    _ = ‖c‖ ^ (p - 1 : ℝ) * ‖c‖ := by rw [Real.rpow_add (by positivity), Real.rpow_one]
+    _ ≤ ‖c‖ ^ (p - 1 : ℝ) * (2 * ‖y‖) := by gcongr; linarith
+    _ = 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 0 := by ring
+    _ ≤ 2 * ‖c‖ ^ (p - 1 : ℝ) * ‖y‖ + 2 ^ (p : ℝ) * ‖y - c‖ ^ (p : ℝ) := by gcongr; positivity
+
+lemma covarianceBilinDual_of_not_memLp' (h : ¬ MemLp (fun x ↦ x - ∫ y, y ∂μ) 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
-  rw [this]
-  exact h_Lp.add (memLp_const _)
+  exact h
+
+@[simp]
+lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
+    covarianceBilinDual μ L₁ L₂ = 0 := by
+  apply covarianceBilinDual_of_not_memLp'
+  contrapose! h
+  exact memLp_id_of_self_sub_integral h
 
 @[simp]
 lemma covarianceBilinDual_zero : covarianceBilinDual (0 : Measure E) = 0 := by
   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 μ
+  by_cases h : MemLp (fun x ↦ x - ∫ y, y ∂μ) 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 _)
+      (measurableEmbedding_subRight _).memLp_map_measure_iff.mpr <| h
     simp_rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply h', mul_comm (L₁ _)]
-  · simp [h]
+  · simp [h, covarianceBilinDual_of_not_memLp']
 
 @[simp]
 lemma covarianceBilinDual_self_nonneg (L : StrongDual ℝ E) : 0 ≤ covarianceBilinDual μ L L := by
@@ -271,7 +324,7 @@ lemma covarianceBilinDual_self_nonneg (L : StrongDual ℝ E) : 0 ≤ covarianceB
     exact real_inner_self_nonneg
   · simp [h]
 
-variable [CompleteSpace E]
+variable [CompleteSpace E] [IsFiniteMeasure μ]
 
 lemma covarianceBilinDual_apply (h : MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) :
     covarianceBilinDual μ L₁ L₂ = ∫ x, (L₁ x - μ[L₁]) * (L₂ x - μ[L₂]) ∂μ := by