chore: drop completeness from the definition of conditional expectation (leanprover-community#39862)

This is not interesting from a mathematical point of view (in all reasonable applications, the spaces are complete), but it is a direct byproduct of the change to `setToFun` in leanprover-community#39615, and it means that whenever we write conditional expectations the job of Lean is easier (as it doesn't have to look for completeness) and the resulting term is simpler.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -82,7 +82,7 @@ variable {α β E 𝕜 : Type*} [RCLike 𝕜] {m m₀ : MeasurableSpace α} {μ
   {s : Set α}
 
 section NormedAddCommGroup
-variable [NormedAddCommGroup E] [CompleteSpace E]
+variable [NormedAddCommGroup E]
 
 section NormedSpace
 variable [NormedSpace ℝ E]
@@ -144,7 +144,8 @@ theorem condExp_const (hm : m ≤ m₀) (c : E) [IsFiniteMeasure μ] :
     μ[fun _ : α ↦ c | m] = fun _ ↦ c :=
   condExp_of_stronglyMeasurable hm stronglyMeasurable_const (integrable_const c)
 
-theorem condExp_ae_eq_condExpL1 (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] (f : α → E) :
+theorem condExp_ae_eq_condExpL1 [CompleteSpace E]
+    (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] (f : α → E) :
     μ[f | m] =ᵐ[μ] condExpL1 hm μ f := by
   rw [condExp_of_sigmaFinite hm]
   by_cases hfi : Integrable f μ
@@ -157,7 +158,8 @@ theorem condExp_ae_eq_condExpL1 (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim h
   rw [if_neg hfi, condExpL1_undef hfi]
   exact (coeFn_zero _ _ _).symm
 
-theorem condExp_ae_eq_condExpL1CLM (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) :
+theorem condExp_ae_eq_condExpL1CLM [CompleteSpace E]
+    (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ) :
     μ[f | m] =ᵐ[μ] condExpL1CLM E hm μ (hf.toL1 f) := by
   refine (condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)
   rw [condExpL1_eq hf]
@@ -189,6 +191,8 @@ theorem stronglyMeasurable_condExp : StronglyMeasurable[m] (μ[f | m]) := by
   · exact aestronglyMeasurable_condExpL1.stronglyMeasurable_mk
   · exact stronglyMeasurable_zero
 
+variable [CompleteSpace E]
+
 @[gcongr]
 theorem condExp_congr_ae (h : f =ᵐ[μ] g) : μ[f | m] =ᵐ[μ] μ[g | m] := by
   by_cases hm : m ≤ m₀
@@ -397,7 +401,7 @@ end RCLike
 end NormedSpace
 
 section Real
-variable [InnerProductSpace ℝ E]
+variable [InnerProductSpace ℝ E] [CompleteSpace E]
 
 -- TODO: Generalize via the conditional Jensen inequality
 lemma eLpNorm_condExp_le : eLpNorm (μ[f | m]) 2 μ ≤ eLpNorm f 2 μ := by
@@ -436,7 +440,7 @@ lemma condExp_ofNat (n : ℕ) [n.AtLeastTwo] (f : α → R) :
 end NormedRing
 
 section NormedLatticeAddCommGroup
-variable [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
+variable [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 /-- **Lebesgue dominated convergence theorem**: sufficient conditions under which almost
   everywhere convergence of a sequence of functions implies the convergence of their image by
@@ -449,6 +453,8 @@ theorem tendsto_condExpL1_of_dominated_convergence (hm : m ≤ m₀) [SigmaFinit
     Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f)) :=
   tendsto_setToFun_of_dominated_convergence _ bound_fs hfs_meas h_int_bound_fs hfs_bound hfs
 
+variable [CompleteSpace E]
+
 /-- If two sequences of functions have a.e. equal conditional expectations at each step, converge
 and verify dominated convergence hypotheses, then the conditional expectations of their limits are
 a.e. equal. -/

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -5,6 +5,7 @@ Authors: Rémy Degenne
 -/
 module
 
+public import Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
 public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
 public import Mathlib.MeasureTheory.Measure.Real
 
@@ -47,7 +48,7 @@ variable {α F F' G G' 𝕜 : Type*} [RCLike 𝕜]
   [NormedSpace 𝕜 F]
   -- F' for integrals on a Lp submodule
   [NormedAddCommGroup F']
-  [NormedSpace 𝕜 F'] [NormedSpace ℝ F'] [CompleteSpace F']
+  [NormedSpace 𝕜 F'] [NormedSpace ℝ F']
   -- G for a Lp add_subgroup
   [NormedAddCommGroup G]
   -- G' for integrals on a Lp add_subgroup
@@ -313,14 +314,18 @@ section CondexpL1
 variable {m m0 : MeasurableSpace α} {μ : Measure α} {hm : m ≤ m0} [SigmaFinite (μ.trim hm)]
   {f g : α → F'} {s : Set α}
 
+section CondExpL1CLM
+
 variable (F')
 
 /-- Conditional expectation of a function as a linear map from `α →₁[μ] F'` to itself. -/
-def condExpL1CLM (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] :
+def condExpL1CLM (hm : m ≤ m0) (μ : Measure α) [CompleteSpace ↑(Lp F' 1 μ)]
+    [SigmaFinite (μ.trim hm)] :
     (α →₁[μ] F') →L[ℝ] α →₁[μ] F' :=
   L1.setToL1 (dominatedFinMeasAdditive_condExpInd F' hm μ)
 
 variable {F'}
+variable [CompleteSpace F']
 
 theorem condExpL1CLM_smul (c : 𝕜) (f : α →₁[μ] F') :
     condExpL1CLM F' hm μ (c • f) = c • condExpL1CLM F' hm μ f := by
@@ -438,17 +443,19 @@ theorem condExpL1CLM_of_aestronglyMeasurable' (f : α →₁[μ] F') (hfm : AESt
     condExpL1CLM F' hm μ f = f :=
   condExpL1CLM_lpMeas (⟨f, hfm⟩ : lpMeas F' ℝ m 1 μ)
 
+end CondExpL1CLM
+
 /-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
 integrable. The function-valued `condExp` should be used instead in most cases. -/
-@[nolint unusedArguments] -- TODO: drop the completeness assumption in the definition, and fix
-def condExpL1 [CompleteSpace F'] (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)]
+def condExpL1 (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)]
     (f : α → F') : α →₁[μ] F' :=
   setToFun μ (condExpInd F' hm μ) (dominatedFinMeasAdditive_condExpInd F' hm μ) f
 
 theorem condExpL1_undef (hf : ¬Integrable f μ) : condExpL1 hm μ f = 0 :=
   setToFun_undef (dominatedFinMeasAdditive_condExpInd F' hm μ) hf
 
-theorem condExpL1_eq (hf : Integrable f μ) : condExpL1 hm μ f = condExpL1CLM F' hm μ (hf.toL1 f) :=
+theorem condExpL1_eq [CompleteSpace F']
+    (hf : Integrable f μ) : condExpL1 hm μ f = condExpL1CLM F' hm μ (hf.toL1 f) :=
   setToFun_eq (dominatedFinMeasAdditive_condExpInd F' hm μ) hf
 
 @[simp]
@@ -459,25 +466,39 @@ theorem condExpL1_zero : condExpL1 hm μ (0 : α → F') = 0 :=
 theorem condExpL1_measure_zero (hm : m ≤ m0) : condExpL1 hm (0 : Measure α) f = 0 :=
   setToFun_measure_zero _ rfl
 
+theorem condExpL1_congr_ae (hm : m ≤ m0) (h : f =ᵐ[μ] g) :
+    condExpL1 hm μ f = condExpL1 hm μ g :=
+  setToFun_congr_ae _ h
+
 theorem aestronglyMeasurable_condExpL1 {f : α → F'} :
     AEStronglyMeasurable[m] (condExpL1 hm μ f) μ := by
-  by_cases hf : Integrable f μ
-  · rw [condExpL1_eq hf]
-    exact aestronglyMeasurable_condExpL1CLM _
+  by_cases hF' : CompleteSpace (Lp F' 1 μ); swap
+  · simp only [condExpL1, setToFun, hF', ↓reduceDIte, ZeroMemClass.coe_zero]
+    apply stronglyMeasurable_zero.aestronglyMeasurable.congr
+    exact (coeFn_zero _ 1 _).symm
+  by_cases hf : Integrable f μ; swap
   · rw [condExpL1_undef hf]
     exact stronglyMeasurable_zero.aestronglyMeasurable.congr (coeFn_zero ..).symm
-
-theorem condExpL1_congr_ae (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (h : f =ᵐ[μ] g) :
-    condExpL1 hm μ f = condExpL1 hm μ g :=
-  setToFun_congr_ae _ h
+  by_cases hf' : f =ᵐ[μ] 0
+  · apply stronglyMeasurable_zero.aestronglyMeasurable.congr
+    simp only [condExpL1_congr_ae hm hf', condExpL1_zero, ZeroMemClass.coe_zero]
+    exact (coeFn_zero _ 1 _).symm
+  have : CompleteSpace F' := by
+    have : Nontrivial (Lp F' 1 μ) := by
+      apply nontrivial_of_ne (hf.toL1 f) 0
+      grw [ne_eq, Lp.ext_iff, Integrable.coeFn_toL1, coeFn_zero]
+      exact hf'
+    exact completeSpace_of_completeSpace_Lp F' 1 μ
+  rw [condExpL1_eq hf]
+  exact aestronglyMeasurable_condExpL1CLM _
 
 theorem integrable_condExpL1 (f : α → F') : Integrable (condExpL1 hm μ f) μ :=
   L1.integrable_coeFn _
 
 /-- The integral of the conditional expectation `condExpL1` over an `m`-measurable set is equal to
 the integral of `f` on that set. See also `setIntegral_condExp`, the similar statement for
 `condExp`. -/
-theorem setIntegral_condExpL1 (hf : Integrable f μ) (hs : MeasurableSet[m] s) :
+theorem setIntegral_condExpL1 [CompleteSpace F'] (hf : Integrable f μ) (hs : MeasurableSet[m] s) :
     ∫ x in s, condExpL1 hm μ f x ∂μ = ∫ x in s, f x ∂μ := by
   simp_rw [condExpL1_eq hf]
   rw [setIntegral_condExpL1CLM (hf.toL1 f) hs]
@@ -498,7 +519,7 @@ theorem condExpL1_sub (hf : Integrable f μ) (hg : Integrable g μ) :
     condExpL1 hm μ (f - g) = condExpL1 hm μ f - condExpL1 hm μ g :=
   setToFun_sub _ hf hg
 
-theorem condExpL1_of_aestronglyMeasurable' (hfm : AEStronglyMeasurable[m] f μ)
+theorem condExpL1_of_aestronglyMeasurable' [CompleteSpace F'] (hfm : AEStronglyMeasurable[m] f μ)
     (hfi : Integrable f μ) : condExpL1 hm μ f =ᵐ[μ] f := by
   rw [condExpL1_eq hfi]
   refine EventuallyEq.trans ?_ (Integrable.coeFn_toL1 hfi)
@@ -507,7 +528,7 @@ theorem condExpL1_of_aestronglyMeasurable' (hfm : AEStronglyMeasurable[m] f μ)
 
 theorem condExpL1_mono {E}
     [NormedAddCommGroup E] [PartialOrder E] [ClosedIciTopology E] [IsOrderedAddMonoid E]
-    [CompleteSpace E] [NormedSpace ℝ E] [IsOrderedModule ℝ E] {f g : α → E} (hf : Integrable f μ)
+    [NormedSpace ℝ E] [IsOrderedModule ℝ E] {f g : α → E} (hf : Integrable f μ)
     (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) :
     condExpL1 hm μ f ≤ᵐ[μ] condExpL1 hm μ g := by
   rw [coeFn_le]

Mathlib/Probability/Martingale/Basic.lean

@@ -46,7 +46,7 @@ open scoped NNReal ENNReal MeasureTheory ProbabilityTheory
 namespace MeasureTheory
 
 variable {Ω E ι : Type*} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω}
-  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0}
+  [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ι → Ω → E} {ℱ : Filtration ι m0}
 
 /-- A family of functions `f : ι → Ω → E` is a martingale with respect to a filtration `ℱ` if `f`
 is strongly adapted with respect to `ℱ` and for all `i ≤ j`, `μ[f j | ℱ i] =ᵐ[μ] f i`. -/
@@ -92,6 +92,8 @@ protected theorem stronglyMeasurable (hf : Martingale f ℱ μ) (i : ι) :
 theorem condExp_ae_eq (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j) : μ[f j | ℱ i] =ᵐ[μ] f i :=
   hf.2 i j hij
 
+variable [CompleteSpace E]
+
 protected theorem integrable (hf : Martingale f ℱ μ) (i : ι) : Integrable (f i) μ :=
   integrable_condExp.congr (hf.condExp_ae_eq (le_refl i))
 
@@ -131,12 +133,12 @@ theorem submartingale [Preorder E] (hf : Martingale f ℱ μ) : Submartingale f
 
 end Martingale
 
-theorem martingale_iff [PartialOrder E] :
+theorem martingale_iff [CompleteSpace E] [PartialOrder E] :
     Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale f ℱ μ :=
   ⟨fun hf => ⟨hf.supermartingale, hf.submartingale⟩, fun ⟨hf₁, hf₂⟩ =>
     ⟨hf₁.1, fun i j hij => (hf₁.2.1 i j hij).antisymm (hf₂.2.1 i j hij)⟩⟩
 
-theorem martingale_condExp (f : Ω → E) (ℱ : Filtration ι m0) (μ : Measure Ω)
+theorem martingale_condExp [CompleteSpace E] (f : Ω → E) (ℱ : Filtration ι m0) (μ : Measure Ω)
     [SigmaFiniteFiltration μ ℱ] : Martingale (fun i => μ[f | ℱ i]) ℱ μ :=
   ⟨fun _ => stronglyMeasurable_condExp, fun _ j hij => condExp_condExp_of_le (ℱ.mono hij) (ℱ.le j)⟩
 
@@ -156,6 +158,8 @@ theorem condExp_ae_le [LE E] (hf : Supermartingale f ℱ μ) {i j : ι} (hij : i
     μ[f j | ℱ i] ≤ᵐ[μ] f i :=
   hf.2.1 i j hij
 
+variable [CompleteSpace E]
+
 theorem setIntegral_le [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
     [ClosedIciTopology E] [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E} (hf : Supermartingale f ℱ μ)
     {i j : ι} (hij : i ≤ j) {s : Set Ω} (hs : MeasurableSet[ℱ i] s) :
@@ -208,6 +212,8 @@ theorem ae_le_condExp [LE E] (hf : Submartingale f ℱ μ) {i j : ι} (hij : i 
     f i ≤ᵐ[μ] μ[f j | ℱ i] :=
   hf.2.1 i j hij
 
+variable [CompleteSpace E]
+
 lemma congr [LE E] (hf : Submartingale f ℱ μ) (hg : StronglyAdapted ℱ g)
     (h_eq : ∀ t, f t =ᵐ[μ] g t) :
     Submartingale g ℱ μ := by
@@ -290,6 +296,8 @@ theorem submartingale_of_setIntegral_le [SigmaFiniteFiltration μ ℱ]
     integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
     setIntegral_condExp (ℱ.le i) (hint j) hs]
 
+variable [CompleteSpace E]
+
 theorem submartingale_of_condExp_sub_nonneg [PartialOrder E] [IsOrderedAddMonoid E]
     [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E} (hadp : StronglyAdapted ℱ f)
     (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i | ℱ i]) :
@@ -319,11 +327,11 @@ end Submartingale
 
 namespace Supermartingale
 
-theorem sub_submartingale [Preorder E] [AddLeftMono E]
+theorem sub_submartingale [CompleteSpace E] [Preorder E] [AddLeftMono E]
     (hf : Supermartingale f ℱ μ) (hg : Submartingale g ℱ μ) : Supermartingale (f - g) ℱ μ := by
   rw [sub_eq_add_neg]; exact hf.add hg.neg
 
-theorem sub_martingale [Preorder E] [AddLeftMono E]
+theorem sub_martingale [CompleteSpace E] [Preorder E] [AddLeftMono E]
     (hf : Supermartingale f ℱ μ) (hg : Martingale g ℱ μ) : Supermartingale (f - g) ℱ μ :=
   hf.sub_submartingale hg.submartingale
 
@@ -398,7 +406,8 @@ end OfSetIntegral
 
 section OfSucc
 
-variable [PartialOrder E] [IsOrderedAddMonoid E] [ClosedIciTopology E] [IsOrderedModule ℝ E]
+variable [CompleteSpace E] [PartialOrder E] [IsOrderedAddMonoid E] [ClosedIciTopology E]
+  [IsOrderedModule ℝ E]
 
 theorem submartingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → E} (hadp : StronglyAdapted 𝒢 f)
     (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, f i ≤ᵐ[μ] μ[f (i + 1) | 𝒢 i]) :
@@ -467,7 +476,8 @@ end Preorder
 
 end SubSuper
 
-theorem martingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → E} (hadp : StronglyAdapted 𝒢 f)
+theorem martingale_nat [CompleteSpace E] [IsFiniteMeasure μ]
+    {f : ℕ → Ω → E} (hadp : StronglyAdapted 𝒢 f)
     (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, f i =ᵐ[μ] μ[f (i + 1) | 𝒢 i]) :
     Martingale f 𝒢 μ := by
   refine ⟨hadp, fun i j hij ↦ ?_⟩
@@ -480,7 +490,7 @@ theorem martingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → E} (hadp : Stron
       with ω hω1 hω2 hω3
     rw [← hω1, hω2, hω3]
 
-theorem martingale_of_setIntegral_eq_succ [IsFiniteMeasure μ] {f : ℕ → Ω → E}
+theorem martingale_of_setIntegral_eq_succ [CompleteSpace E] [IsFiniteMeasure μ] {f : ℕ → Ω → E}
     (hadp : StronglyAdapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
     (hf : ∀ i, ∀ s : Set Ω, MeasurableSet[𝒢 i] s → ∫ ω in s, f i ω ∂μ = ∫ ω in s, f (i + 1) ω ∂μ) :
     Martingale f 𝒢 μ := by
@@ -491,7 +501,7 @@ theorem martingale_of_setIntegral_eq_succ [IsFiniteMeasure μ] {f : ℕ → Ω 
     ← setIntegral_trim (𝒢.le n) stronglyMeasurable_condExp ms,
     setIntegral_condExp (𝒢.le n) (hint (n + 1)) ms, hf n s ms]
 
-theorem martingale_of_condExp_sub_eq_zero_nat [IsFiniteMeasure μ] {f : ℕ → Ω → E}
+theorem martingale_of_condExp_sub_eq_zero_nat [CompleteSpace E] [IsFiniteMeasure μ] {f : ℕ → Ω → E}
     (hadp : StronglyAdapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
     (hf : ∀ i, μ[f (i + 1) - f i | 𝒢 i] =ᵐ[μ] 0) : Martingale f 𝒢 μ := by
   refine martingale_nat hadp hint fun i ↦ ?_
@@ -500,7 +510,8 @@ theorem martingale_of_condExp_sub_eq_zero_nat [IsFiniteMeasure μ] {f : ℕ →
   exact EventuallyEq.trans (condExp_sub (hint _) (hint _) _).symm (hf i)
 
 /-- A predictable martingale is a.e. equal to its initial state. -/
-theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
+theorem Martingale.eq_zero_of_predictable [CompleteSpace E] [SigmaFiniteFiltration μ 𝒢]
+    {f : ℕ → Ω → E}
     (hfmgle : Martingale f 𝒢 μ) (hfadp : StronglyAdapted 𝒢 fun n => f (n + 1)) (n : ℕ) :
     f n =ᵐ[μ] f 0 := by
   induction n with
@@ -511,7 +522,7 @@ theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : 
 
 section IsStronglyPredictable
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 /-- A predictable submartingale is a.e. greater than or equal to its initial state. -/
 theorem Submartingale.zero_le_of_predictable' [Preorder E] [SigmaFiniteFiltration μ 𝒢]
@@ -526,7 +537,8 @@ theorem Supermartingale.le_zero_of_predictable' [Preorder E] [SigmaFiniteFiltrat
   le_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
 /-- A predictable martingale is a.e. equal to its initial state. -/
-theorem Martingale.eq_zero_of_predictable' [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
+theorem Martingale.eq_zero_of_predictable' [CompleteSpace E] [SigmaFiniteFiltration μ 𝒢]
+    {f : ℕ → Ω → E}
     (hfmgle : Martingale f 𝒢 μ) (hfadp : IsStronglyPredictable 𝒢 f) (n : ℕ) : f n =ᵐ[μ] f 0 :=
   eq_zero_of_predictable hfmgle hfadp.measurable_add_one n
 
@@ -543,9 +555,11 @@ end Submartingale
 
 section SumSMul
 
-variable [PartialOrder E] [IsOrderedModule ℝ E] [ClosedIciTopology E] [IsOrderedAddMonoid E]
+variable [CompleteSpace E] [PartialOrder E] [IsOrderedModule ℝ E] [ClosedIciTopology E]
+  [IsOrderedAddMonoid E]
 
-theorem Submartingale.sum_smul_sub [IsFiniteMeasure μ] {R : ℝ} {f : ℕ → Ω → E} {ξ : ℕ → Ω → ℝ}
+theorem Submartingale.sum_smul_sub [IsFiniteMeasure μ] {R : ℝ}
+    {f : ℕ → Ω → E} {ξ : ℕ → Ω → ℝ}
     (hf : Submartingale f 𝒢 μ) (hξ : StronglyAdapted 𝒢 ξ) (hbdd : ∀ n ω, ξ n ω ≤ R)
     (hnonneg : ∀ n ω, 0 ≤ ξ n ω) :
     Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ := by