diff --git a/BrownianMotion/StochasticIntegral/DoobMeyer.lean b/BrownianMotion/StochasticIntegral/DoobMeyer.lean
index ad02d06b..87de961c 100644
--- a/BrownianMotion/StochasticIntegral/DoobMeyer.lean
+++ b/BrownianMotion/StochasticIntegral/DoobMeyer.lean
@@ -22,6 +22,12 @@ import Mathlib.Order.CompleteLattice.Group
 open MeasureTheory Filter Order ProbabilityTheory Convexity
 open scoped NNReal ENNReal Topology
 
+/-- An element of `WithTop α` other than `⊤` is at most the coercion of `⊤ : α`. -/
+lemma WithTop.le_coe_top {α : Type*} [Preorder α] [OrderTop α] {x : WithTop α} (hx : x ≠ ⊤) :
+    x ≤ ((⊤ : α) : WithTop α) := by
+  lift x to α using hx
+  exact mod_cast le_top
+
 section DenseMesh
 
 /-- The fixed countable dense set used instead of dyadics, with both endpoints adjoined. -/
@@ -44,11 +50,27 @@ noncomputable def denseEnum (ι : Type*) [LE ι] [OrderBot ι] [OrderTop ι]
   have : Nonempty (denseSet ι) := ⟨⟨⊥, by simp [denseSet]⟩⟩
   Subtype.val ∘ (countable_iff_exists_surjective.mp (denseSet_countable ι)).choose
 
+/-- Every element of the dense set is attained by the enumeration. -/
+lemma exists_denseEnum_eq (ι : Type*) [LE ι] [OrderBot ι] [OrderTop ι]
+    [TopologicalSpace ι] [SecondCountableTopology ι] {d : ι} (hd : d ∈ denseSet ι) :
+    ∃ k, denseEnum ι k = d := by
+  have : Nonempty (denseSet ι) := ⟨⟨⊥, by simp [denseSet]⟩⟩
+  obtain ⟨k, hk⟩ :=
+    (countable_iff_exists_surjective.mp (denseSet_countable ι)).choose_spec ⟨d, hd⟩
+  exact ⟨k, congrArg Subtype.val hk⟩
+
 /-- The `n`-th finite mesh: the first `n` points of the dense enumeration, plus endpoints. -/
 noncomputable def mesh (ι : Type*) [LinearOrder ι] [OrderBot ι] [OrderTop ι]
     [TopologicalSpace ι] [SecondCountableTopology ι] (n : ℕ) : Finset ι :=
   insert ⊥ <| insert ⊤ <| (Finset.range n).image (denseEnum ι)
 
+/-- The `k`-th point of the dense enumeration belongs to all meshes past `k`. -/
+lemma denseEnum_mem_mesh (ι : Type*) [LinearOrder ι] [OrderBot ι] [OrderTop ι]
+    [TopologicalSpace ι] [SecondCountableTopology ι] {k n : ℕ} (hkn : k < n) :
+    denseEnum ι k ∈ mesh ι n := by
+  simp only [mesh, Finset.mem_insert, Finset.mem_image]
+  exact .inr <| .inr ⟨k, Finset.mem_range.2 hkn, rfl⟩
+
 lemma bot_mem_mesh (ι : Type*) [LinearOrder ι] [OrderBot ι] [OrderTop ι]
     [TopologicalSpace ι] [SecondCountableTopology ι] (n : ℕ) : (⊥ : ι) ∈ mesh ι n := by simp [mesh]
 
@@ -281,6 +303,29 @@ lemma martingaleSeqTop_eq_neg_predictableSeqTop {ι Ω E : Type*} [TopologicalSp
     predictableSeqTop]
   grw [neg_eq_zero_sub, hstop]
 
+/-- The terminal values of the martingale parts on each mesh are integrable. -/
+lemma integrable_martingaleSeqTop {ι Ω E : Type*} [TopologicalSpace ι]
+    [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]
+    {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    [CompleteSpace E] {S : ι → Ω → E} (𝓕 : Filtration ι mΩ) (hS : Integrable (S ⊤) P) (n : ℕ) :
+    Integrable (martingaleSeqTop S 𝓕 P n) P := by
+  simpa [martingaleSeqTop, _root_.martingalePart, predictableSeqTop] using
+    hS.sub (integrable_predictableSeqTop S 𝓕 P n)
+
+/-- On each mesh, the terminal value of the martingale part has the same expectation as the
+initial value of the process. -/
+lemma integral_martingaleSeqTop {ι Ω E : Type*} [TopologicalSpace ι] [SecondCountableTopology ι]
+    [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω}
+    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E}
+    (𝓕 : Filtration ι mΩ) [SigmaFiniteFiltration P 𝓕] (n : ℕ) :
+    ∫ ω, martingaleSeqTop S 𝓕 P n ω ∂P = ∫ ω, S ⊥ ω ∂P := by
+  calc ∫ ω, martingaleSeqTop S 𝓕 P n ω ∂P
+      = ∫ ω, (P[martingaleSeqTop S 𝓕 P n|meshFiltration 𝓕 n ⊥]) ω ∂P :=
+        (integral_condExp ((meshFiltration 𝓕 n).le ⊥)).symm
+    _ = ∫ ω, martingalePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P ⊥ ω ∂P :=
+        integral_congr_ae ((martingale_martingalePart _ _ _).condExp_ae_eq bot_le)
+    _ = ∫ ω, S ⊥ ω ∂P := by simp [_root_.martingalePart]
+
 /-- Apply the optional stopping theorem to get equation 4. Note that `T1 Space` is needed to make
 sure that `mesh ι n` has order topology. -/
 lemma equation4 {ι Ω E : Type*} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι]
@@ -764,29 +809,44 @@ end UniformIntegrability
 -- We define the martingale part in the doob-meyer decomposition.
 section MartingalePartLimDef
 
-/-- Show that the terminals values of some convex combinations of the martingale parts converge. -/
+/-- Show that the terminals values of some convex combinations of the martingale parts converge.
+The convex combination at step `n` only involves meshes of index at least `n`, as provided by
+`komlos_L1`. -/
 lemma exists_martingalPart_lim {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]
     {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}
     {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) :
-    ∃ M : Ω → ℝ, ∃ a : ℕ → StdSimplex ℝ ℕ,
+    ∃ M : Ω → ℝ, ∃ a : ℕ → StdSimplex ℝ ℕ, Integrable M P ∧
+      (∀ n, ∀ m < n, (a n).weights m = 0) ∧
       Tendsto (fun n ↦ eLpNorm ((a n).weights.sum (fun m r ↦ r • martingaleSeqTop S 𝓕 P m) - M) 1 P)
       atTop (𝓝 0) := by
-  sorry
+  obtain ⟨g, M, hM, h_convex, h_tendsto⟩ :=
+    komlos_L1 (uniformIntegrable_martingaleSeqTop hd.uniformIntegrable hs)
+  choose a ha h0 using fun n ↦
+    exists_stdSimplex_of_mem_convexTail_reindexed (x := martingaleSeqTop S 𝓕 P) h_convex n
+  exact ⟨M, a, memLp_one_iff_integrable.1 hM, h0, h_tendsto.congr fun n ↦ by rw [ha n]⟩
+
+/-- The `L¹` limit of the convex combinations of the terminal values of the discrete martingale
+parts, given by `exists_martingalPart_lim`. -/
+noncomputable def martingaleLim {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
+    [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]
+    {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}
+    {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) : Ω → ℝ :=
+  (exists_martingalPart_lim hd hs).choose
 
 /-- This is the martingalePart in the doob-meyer decomposition of a submartingale. -/
 noncomputable def martingalePartLim {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]
     {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}
     {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) (i : ι) :=
-  P[(exists_martingalPart_lim hd hs).choose | 𝓕 i]
+  P[martingaleLim hd hs | 𝓕 i]
 
 lemma martingale_martingalePartLim {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
     [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι]
     {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}
     {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) :
     Martingale (martingalePartLim hd hs) 𝓕 P :=
-  martingale_condExp (exists_martingalPart_lim hd hs).choose 𝓕 P
+  martingale_condExp (martingaleLim hd hs) 𝓕 P
 
 /-- This is the weight associated with the martingale part. -/
 noncomputable def weight {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
@@ -795,6 +855,56 @@ noncomputable def weight {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι]
     {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) : ℕ → StdSimplex ℝ ℕ :=
   (exists_martingalPart_lim hd hs).choose_spec.choose
 
+section
+
+variable {ι Ω : Type*} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι]
+  [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω}
+  {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ}
+
+/-- The limit of the convex combinations of the terminal martingale parts is integrable. -/
+lemma integrable_martingaleLim (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) :
+    Integrable (martingaleLim hd hs) P :=
+  (exists_martingalPart_lim hd hs).choose_spec.choose_spec.1
+
+/-- The Komlós weights at step `n` vanish on meshes of index below `n`. -/
+lemma weight_apply_eq_zero_of_lt (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) {m n : ℕ}
+    (hmn : m < n) : (weight hd hs n).weights m = 0 :=
+  (exists_martingalPart_lim hd hs).choose_spec.choose_spec.2.1 n m hmn
+
+/-- `L¹` convergence of the convex combinations of the terminal martingale parts to
+`martingaleLim`. -/
+lemma tendsto_eLpNorm_weight_sum_martingaleSeqTop (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) :
+    Tendsto (fun n ↦ eLpNorm ((weight hd hs n).weights.sum
+      (fun m r ↦ r • martingaleSeqTop S 𝓕 P m) - martingaleLim hd hs) 1 P) atTop (𝓝 0) :=
+  (exists_martingalPart_lim hd hs).choose_spec.choose_spec.2.2
+
+/-- Each conditional expectation defining the martingale part of the decomposition has the same
+expectation as the initial value of the process. -/
+lemma integral_martingalePartLim (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) (i : ι) :
+    ∫ ω, martingalePartLim hd hs i ω ∂P = ∫ ω, S ⊥ ω ∂P := by
+  have hint (m : ℕ) : Integrable (martingaleSeqTop S 𝓕 P m) P :=
+    integrable_martingaleSeqTop 𝓕 (hs.integrable ⊤) m
+  have hg (n : ℕ) : ∫ ω, ((weight hd hs n).weights.sum
+      fun m r ↦ r • martingaleSeqTop S 𝓕 P m) ω ∂P = ∫ ω, S ⊥ ω ∂P := by
+    have htotal : ∑ m ∈ (weight hd hs n).weights.support, (weight hd hs n).weights m = 1 := by
+      simpa [Finsupp.sum] using (weight hd hs n).total
+    simp only [Finsupp.sum, Finset.sum_apply]
+    rw [integral_finsetSum _ fun m _ ↦ (hint m).smul _]
+    simp_rw [Pi.smul_apply, integral_smul, integral_martingaleSeqTop]
+    rw [← Finset.sum_smul, htotal, one_smul]
+  have hlim : Tendsto (fun n ↦ ∫ ω, ((weight hd hs n).weights.sum
+      fun m r ↦ r • martingaleSeqTop S 𝓕 P m) ω ∂P) atTop
+      (𝓝 (∫ ω, martingaleLim hd hs ω ∂P)) :=
+    tendsto_integral_of_L1' _ (integrable_martingaleLim hd hs).aestronglyMeasurable
+      (.of_forall fun n ↦ integrable_finsetSum' _ fun m _ ↦ (hint m).smul _)
+      (tendsto_eLpNorm_weight_sum_martingaleSeqTop hd hs)
+  rw [martingalePartLim, integral_condExp (𝓕.le i)]
+  refine tendsto_nhds_unique hlim ?_
+  simp_rw [hg]
+  exact tendsto_const_nhds
+
+end
+
 /-- The extension of the discrete martingale part `M^n`. -/
 noncomputable def martingaleSeqStep {ι Ω : Type*} [TopologicalSpace ι] [SecondCountableTopology ι]
     [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} (P : Measure Ω)
@@ -873,6 +983,215 @@ lemma predictableConvexStep_ae_tendsto {ι Ω : Type*} [TopologicalSpace ι] [T1
 
 end PredictablePartLimDef
 
+-- We discretize a stopping time from the right along the meshes.
+section MeshCeil
+
+variable {ι Ω : Type*} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι]
+  [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ}
+  {𝓕 : Filtration ι mΩ} {τ : Ω → WithTop ι}
+
+/-- The discretization `σₙ` of a stopping time `τ` from the right along the `n`-th mesh: the
+smallest mesh point greater than or equal to `τ`, or `⊤` if `τ = ⊤`. -/
+noncomputable def meshCeil (n : ℕ) (τ : Ω → WithTop ι) : Ω → WithTop ι :=
+  fun ω ↦ ((mesh ι n).filter fun u : ι ↦ τ ω ≤ (u : WithTop ι)).min
+
+lemma le_meshCeil (n : ℕ) (ω : Ω) : τ ω ≤ meshCeil n τ ω :=
+  Finset.le_min fun _ hu ↦ (Finset.mem_filter.1 hu).2
+
+lemma meshCeil_le {n : ℕ} {ω : Ω} {u : ι} (hu : u ∈ mesh ι n) (hτu : τ ω ≤ (u : WithTop ι)) :
+    meshCeil n τ ω ≤ (u : WithTop ι) :=
+  Finset.min_le (Finset.mem_filter.2 ⟨hu, hτu⟩)
+
+lemma meshCeil_ne_top (n : ℕ) {ω : Ω} (hτ : τ ω ≠ ⊤) : meshCeil n τ ω ≠ ⊤ := by
+  intro h
+  simp only [meshCeil, Finset.min_eq_top, Finset.filter_eq_empty_iff] at h
+  exact h (top_mem_mesh ι n) (WithTop.le_coe_top hτ)
+
+lemma mesh_mem_of_meshCeil_eq_coe {n : ℕ} {ω : Ω} {u : ι}
+    (h : meshCeil n τ ω = (u : WithTop ι)) :
+    u ∈ mesh ι n ∧ τ ω ≤ (u : WithTop ι) :=
+  Finset.mem_filter.1 <| Finset.mem_of_min h
+
+lemma exists_meshCeil_eq_coe (n : ℕ) {ω : Ω} (hτ : τ ω ≠ ⊤) :
+    ∃ u ∈ mesh ι n, meshCeil n τ ω = (u : WithTop ι) ∧ τ ω ≤ (u : WithTop ι) := by
+  obtain ⟨u, hu⟩ := WithTop.ne_top_iff_exists.1 (meshCeil_ne_top n hτ)
+  obtain ⟨h1, h2⟩ := mesh_mem_of_meshCeil_eq_coe hu.symm
+  exact ⟨u, h1, hu.symm, h2⟩
+
+lemma meshCeil_eq_bot {n : ℕ} {ω : Ω} (h : τ ω = ((⊥ : ι) : WithTop ι)) :
+    meshCeil n τ ω = ((⊥ : ι) : WithTop ι) :=
+  le_antisymm (meshCeil_le (bot_mem_mesh ι n) h.le) (h ▸ le_meshCeil n ω)
+
+lemma countable_range_meshCeil (n : ℕ) (τ : Ω → WithTop ι) :
+    (Set.range (meshCeil n τ)).Countable := by
+  refine ((((mesh ι n).image fun u : ι ↦ (u : WithTop ι)).countable_toSet).insert ⊤).mono ?_
+  rintro x ⟨ω, rfl⟩
+  rcases eq_or_ne (meshCeil n τ ω) ⊤ with h | h
+  · exact h ▸ Set.mem_insert _ _
+  · obtain ⟨u, hu⟩ := WithTop.ne_top_iff_exists.1 h
+    exact hu ▸ Set.mem_insert_of_mem _
+      (Finset.mem_coe.2 (Finset.mem_image_of_mem _ (mesh_mem_of_meshCeil_eq_coe hu.symm).1))
+
+/-- The mesh discretization of a stopping time is a stopping time. -/
+lemma isStoppingTime_meshCeil (hτ : IsStoppingTime 𝓕 τ) (n : ℕ) :
+    IsStoppingTime 𝓕 (meshCeil n τ) := by
+  intro t
+  have h_eq : {ω | meshCeil n τ ω ≤ t}
+      = ⋃ u ∈ {u ∈ mesh ι n | u ≤ t}, {ω | τ ω ≤ (u : WithTop ι)} := by
+    ext ω
+    simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Finset.mem_filter, exists_prop]
+    constructor
+    · intro h
+      rcases eq_or_ne (meshCeil n τ ω) ⊤ with htop | htop
+      · rw [htop] at h
+        exact absurd (top_le_iff.1 h) WithTop.coe_ne_top
+      · obtain ⟨u, hu⟩ := WithTop.ne_top_iff_exists.1 htop
+        obtain ⟨h1, h2⟩ := mesh_mem_of_meshCeil_eq_coe hu.symm
+        exact ⟨u, ⟨h1, WithTop.coe_le_coe.1 (hu.le.trans h)⟩, h2⟩
+    · rintro ⟨u, ⟨hu_mesh, hut⟩, hτu⟩
+      exact (meshCeil_le hu_mesh hτu).trans (WithTop.coe_le_coe.2 hut)
+  rw [h_eq]
+  exact Finset.measurableSet_biUnion _ fun u hu ↦
+    𝓕.mono (Finset.mem_filter.1 hu).2 _ (hτ u)
+
+/-- The mesh discretizations of `τ` converge to `τ` from the right. -/
+lemma tendsto_untopA_meshCeil [OrderTopology ι] [DenselyOrdered ι] {ω : Ω} (hτ : τ ω ≠ ⊤) :
+    Tendsto (fun n ↦ (meshCeil n τ ω).untopA) atTop (𝓝[≥] (τ ω).untopA) := by
+  obtain ⟨t₀, ht₀⟩ := WithTop.ne_top_iff_exists.1 hτ
+  have hle (n : ℕ) : t₀ ≤ (meshCeil n τ ω).untopA :=
+    (WithTop.le_untopA_iff (meshCeil_ne_top n hτ)).2 (ht₀.le.trans (le_meshCeil n ω))
+  rw [← ht₀, WithTop.untopA_coe, tendsto_nhdsWithin_iff]
+  refine ⟨tendsto_order.2 ⟨fun a ha ↦ Eventually.of_forall fun n ↦ ha.trans_le (hle n),
+    fun b hb ↦ ?_⟩, Eventually.of_forall fun n ↦ hle n⟩
+  obtain ⟨d, hd_mem, hd₁, hd₂⟩ : ∃ d ∈ denseSet ι, t₀ < d ∧ d < b := by
+    obtain ⟨c, hc₁, hc₂⟩ := exists_between hb
+    obtain ⟨d, hd_mem, hd⟩ := (denseSet_dense ι).exists_mem_open isOpen_Ioo ⟨c, hc₁, hc₂⟩
+    exact ⟨d, hd_mem, hd.1, hd.2⟩
+  obtain ⟨k, hk⟩ := exists_denseEnum_eq ι hd_mem
+  filter_upwards [eventually_gt_atTop k] with n hn
+  have hceil : meshCeil n τ ω ≤ (d : WithTop ι) :=
+    meshCeil_le (hk ▸ denseEnum_mem_mesh ι hn) (ht₀ ▸ WithTop.coe_le_coe.2 hd₁.le)
+  exact ((WithTop.untopA_le_iff (meshCeil_ne_top n hτ)).2 hceil).trans_lt hd₂
+
+/-- On the half-open mesh interval `(pred u, u]`, the step extension of the discrete predictable
+part takes the value of the discrete predictable part at `u`. -/
+lemma predictableSeqStep_apply_of_mem {n : ℕ} {t : ι} {u : mesh ι n} (ht : t ∈ meshPredIoc n u) :
+    predictableSeqStep P S 𝓕 n t
+      = predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u := by
+  rw [predictableSeqStep, Finset.sum_eq_single u]
+  · rw [Set.indicator_of_mem ht]
+  · refine fun v _ hvu ↦ Set.indicator_of_notMem (fun htv ↦ ?_) _
+    rcases lt_or_gt_of_ne hvu with h | h
+    · exact absurd (htv.2.trans (Subtype.coe_le_coe.2 (le_pred_of_lt h))) (not_le.2 ht.1)
+    · exact absurd (ht.2.trans (Subtype.coe_le_coe.2 (le_pred_of_lt h))) (not_le.2 htv.1)
+  · exact fun hu ↦ absurd (Finset.mem_univ u) hu
+
+/-- Sampling the step extension of the discrete predictable part at `τ` is the same as sampling
+it at the mesh discretization `σₙ` of `τ`. -/
+lemma stoppedValue_predictableSeqStep_meshCeil {n : ℕ} (hτ_ne : ∀ ω, τ ω ≠ ⊤) :
+    stoppedValue (predictableSeqStep P S 𝓕 n) τ
+      = stoppedValue (predictableSeqStep P S 𝓕 n) (meshCeil n τ) := by
+  funext ω
+  obtain ⟨t, ht⟩ := WithTop.ne_top_iff_exists.1 (hτ_ne ω)
+  obtain ⟨u, humesh, hcoe, hle⟩ := exists_meshCeil_eq_coe n (hτ_ne ω)
+  simp only [stoppedValue, hcoe, ← ht, WithTop.untopA_coe]
+  rcases eq_or_ne t ⊥ with rfl | ht_bot
+  · rw [WithTop.coe_injective (hcoe.symm.trans (meshCeil_eq_bot ht.symm))]
+  · have htu : t ≤ u := WithTop.coe_le_coe.1 (ht.trans_le hle)
+    have hu_bot : (⟨u, humesh⟩ : mesh ι n) ≠ ⊥ :=
+      fun h ↦ ht_bot (le_bot_iff.1 (htu.trans_eq (congrArg Subtype.val h)))
+    have hpred : ((pred (⟨u, humesh⟩ : mesh ι n) : mesh ι n) : ι) < t := by
+      by_contra hcon
+      rw [not_lt] at hcon
+      have h2 := meshCeil_le (pred (⟨u, humesh⟩ : mesh ι n)).2
+        (le_trans (le_of_eq ht.symm) (by exact_mod_cast hcon))
+      rw [hcoe, WithTop.coe_le_coe] at h2
+      exact absurd (Subtype.coe_le_coe.1 h2) (not_le.2 (pred_lt_iff_ne_bot.2 hu_bot))
+    rw [predictableSeqStep_apply_of_mem (u := ⟨u, humesh⟩) ⟨hpred, htu⟩,
+      predictableSeqStep_apply_of_mem (u := ⟨u, humesh⟩)
+        ⟨Subtype.coe_lt_coe.2 (pred_lt_iff_ne_bot.2 hu_bot), le_rfl⟩]
+
+/-- Sampled at the mesh discretization `σₙ`, the step extension of the discrete predictable part
+decomposes as the sampled process minus the sampled conditional expectations of the terminal
+value of the discrete martingale part. -/
+lemma stoppedValue_predictableSeqStep_ae_eq {n : ℕ} (hτ_ne : ∀ ω, τ ω ≠ ⊤) :
+    stoppedValue (predictableSeqStep P S 𝓕 n) (meshCeil n τ) =ᵐ[P]
+      stoppedValue S (meshCeil n τ)
+        - stoppedValue (martingaleSeqStep P S 𝓕 n) (meshCeil n τ) := by
+  have hkey : ∀ᵐ ω ∂P, ∀ u : mesh ι n,
+      martingalePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u ω
+        = martingaleSeqStep P S 𝓕 n ↑u ω :=
+    ae_all_iff.2 fun u ↦
+      ((martingale_martingalePart _ _ _).condExp_ae_eq (le_top (a := u))).symm
+  filter_upwards [hkey] with ω hω
+  obtain ⟨u, humesh, hcoe, hle⟩ := exists_meshCeil_eq_coe n (hτ_ne ω)
+  simp only [stoppedValue, hcoe, WithTop.untopA_coe, Pi.sub_apply]
+  calc predictableSeqStep P S 𝓕 n u ω
+      = predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P ⟨u, humesh⟩ ω := by
+        rcases eq_or_ne (⟨u, humesh⟩ : mesh ι n) ⊥ with h | h
+        · have hu : u = ⊥ := by simpa using congrArg Subtype.val h
+          rw [h, hu]
+          simp [predictableSeqStep, meshPredIoc]
+        · rw [predictableSeqStep_apply_of_mem
+            ⟨Subtype.coe_lt_coe.2 (pred_lt_iff_ne_bot.2 h), le_rfl⟩]
+    _ = S u ω - martingalePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P ⟨u, humesh⟩ ω :=
+        eq_sub_of_add_eq' (congrFun (congrFun
+          (martingalePart_add_predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P) _) ω)
+    _ = S u ω - martingaleSeqStep P S 𝓕 n u ω := by rw [hω ⟨u, humesh⟩]
+
+/-- The expectation of the stopped step extension of the discrete predictable part. -/
+lemma integral_stoppedValue_predictableSeqStep [OrderTopology ι] [MeasurableSpace ι]
+    [IsFiniteMeasure P]
+    (hd : ClassD S 𝓕 P) (hτ : IsStoppingTime 𝓕 τ) (hτ_ne : ∀ ω, τ ω ≠ ⊤) (n : ℕ) :
+    ∫ ω, stoppedValue (predictableSeqStep P S 𝓕 n) τ ω ∂P
+      = ∫ ω, stoppedValue S (meshCeil n τ) ω ∂P - ∫ ω, S ⊥ ω ∂P := by
+  have hσ : IsStoppingTime 𝓕 (meshCeil n τ) := isStoppingTime_meshCeil hτ n
+  have hσ_ne (ω) : meshCeil n τ ω ≠ ⊤ := meshCeil_ne_top n (hτ_ne ω)
+  have hσ_le (ω) : meshCeil n τ ω ≤ ((⊤ : ι) : WithTop ι) := WithTop.le_coe_top (hσ_ne ω)
+  have hN : Martingale (martingaleSeqStep P S 𝓕 n) 𝓕 P := martingale_condExp _ _ _
+  have hint_S : Integrable (stoppedValue S (meshCeil n τ)) P :=
+    memLp_one_iff_integrable.1 (hd.uniformIntegrable.memLp ⟨_, hσ, hσ_ne⟩)
+  have hint_N : Integrable (stoppedValue (martingaleSeqStep P S 𝓕 n) (meshCeil n τ)) P :=
+    hN.integrable_stoppedValue_of_countable_range _ hσ hσ_le (countable_range_meshCeil n τ)
+  rw [stoppedValue_predictableSeqStep_meshCeil hτ_ne,
+    integral_congr_ae (stoppedValue_predictableSeqStep_ae_eq hτ_ne)]
+  simp only [Pi.sub_apply]
+  rw [integral_sub hint_S hint_N]
+  congr 1
+  calc ∫ ω, stoppedValue (martingaleSeqStep P S 𝓕 n) (meshCeil n τ) ω ∂P
+      = ∫ ω, (P[martingaleSeqStep P S 𝓕 n ⊤|hσ.measurableSpace]) ω ∂P := integral_congr_ae <|
+        hN.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ hσ_le
+          (countable_range_meshCeil n τ)
+    _ = ∫ ω, P[martingaleSeqTop S 𝓕 P n|𝓕 ⊤] ω ∂P := integral_condExp _
+    _ = ∫ ω, martingaleSeqTop S 𝓕 P n ω ∂P := integral_condExp (𝓕.le ⊤)
+    _ = ∫ ω, S ⊥ ω ∂P := integral_martingaleSeqTop 𝓕 n
+
+/-- Expectations of the process sampled at the mesh discretizations of `τ` converge to the
+expectation of the process sampled at `τ`. -/
+lemma tendsto_integral_stoppedValue_meshCeil [OrderTopology ι] [DenselyOrdered ι]
+    [MeasurableSpace ι] [IsFiniteMeasure P]
+    (hd : ClassD S 𝓕 P) (hτ : IsStoppingTime 𝓕 τ) (hτ_ne : ∀ ω, τ ω ≠ ⊤)
+    (hc : ∀ᵐ ω ∂P, IsCadlag (S · ω)) :
+    Tendsto (fun n ↦ ∫ ω, stoppedValue S (meshCeil n τ) ω ∂P) atTop
+      (𝓝 (∫ ω, stoppedValue S τ ω ∂P)) := by
+  have hUI : UniformIntegrable (fun n ↦ stoppedValue S (meshCeil n τ)) 1 P :=
+    hd.uniformIntegrable.comp fun n ↦ ⟨meshCeil n τ, isStoppingTime_meshCeil hτ n,
+      fun ω ↦ meshCeil_ne_top n (hτ_ne ω)⟩
+  have hmem : MemLp (stoppedValue S τ) 1 P := hd.uniformIntegrable.memLp ⟨τ, hτ, hτ_ne⟩
+  have hae : ∀ᵐ ω ∂P, Tendsto (fun n ↦ stoppedValue S (meshCeil n τ) ω) atTop
+      (𝓝 (stoppedValue S τ ω)) := by
+    filter_upwards [hc] with ω hcad
+    exact Tendsto.comp (continuousWithinAt_Ioi_iff_Ici.1 (hcad.right_continuous ((τ ω).untopA)))
+      (tendsto_untopA_meshCeil (hτ_ne ω))
+  have hL1 : Tendsto (fun n ↦ eLpNorm (stoppedValue S (meshCeil n τ) - stoppedValue S τ) 1 P)
+      atTop (𝓝 0) :=
+    tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hUI.1 hmem hUI.2.1
+      (tendstoInMeasure_of_tendsto_ae hUI.1 hae)
+  exact tendsto_integral_of_L1' _ hmem.aestronglyMeasurable
+    (.of_forall fun n ↦ memLp_one_iff_integrable.1 (hUI.memLp n)) hL1
+
+end MeshCeil
+
 -- Helper lemmas about limits of monotone functions.
 section MonotoneLim
 
@@ -1243,10 +1562,53 @@ lemma integral_stoppedValue_predictableConvexStep_tendsto_stoppedValue_predictab
     [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι]
     {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ}
     {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P) (hs : Submartingale S 𝓕 P) {τ : Ω → WithTop ι}
-    (hτ : IsStoppingTime 𝓕 τ) :
-    Tendsto (fun n => ∫ ω, stoppedValue (predictableConvexStep hd hs n) τ ω ∂P) atTop
+    (hτ : IsStoppingTime 𝓕 τ) (hτ_ne : ∀ ω, τ ω ≠ ⊤) (hτ_count : (Set.range τ).Countable)
+    (hc : ∀ᵐ ω ∂P, IsCadlag (S · ω)) :
+    Tendsto (fun n ↦ ∫ ω, stoppedValue (predictableConvexStep hd hs n) τ ω ∂P) atTop
       (𝓝 <| ∫ ω, stoppedValue (predictablePartLim hd hs) τ ω ∂P) := by
-  sorry
+  have hint (m : ℕ) : Integrable (stoppedValue (predictableSeqStep P S 𝓕 m) τ) P := by
+    have hσ : IsStoppingTime 𝓕 (meshCeil m τ) := isStoppingTime_meshCeil hτ m
+    have hσ_ne (ω) : meshCeil m τ ω ≠ ⊤ := meshCeil_ne_top m (hτ_ne ω)
+    have hS : Integrable (stoppedValue S (meshCeil m τ)) P :=
+      memLp_one_iff_integrable.1 (hd.uniformIntegrable.memLp ⟨_, hσ, hσ_ne⟩)
+    have hN : Integrable (stoppedValue (martingaleSeqStep P S 𝓕 m) (meshCeil m τ)) P :=
+      (martingale_condExp _ _ _).integrable_stoppedValue_of_countable_range _ hσ
+        (fun ω ↦ WithTop.le_coe_top (hσ_ne ω)) (countable_range_meshCeil m τ)
+    rw [stoppedValue_predictableSeqStep_meshCeil hτ_ne]
+    exact (integrable_congr (stoppedValue_predictableSeqStep_ae_eq hτ_ne).symm).1 (hS.sub hN)
+  have h1 (n : ℕ) : ∫ ω, stoppedValue (predictableConvexStep hd hs n) τ ω ∂P
+      = ((weight hd hs n).weights.sum
+          fun m r ↦ r • ∫ ω, stoppedValue S (meshCeil m τ) ω ∂P) - ∫ ω, S ⊥ ω ∂P := by
+    have hstop : stoppedValue (predictableConvexStep hd hs n) τ
+        = ∑ m ∈ (weight hd hs n).weights.support,
+            (weight hd hs n).weights m • stoppedValue (predictableSeqStep P S 𝓕 m) τ := by
+      funext ω
+      simp [predictableConvexStep, stoppedValue, Finsupp.sum, Finset.sum_apply]
+    rw [hstop]
+    simp only [Finset.sum_apply]
+    rw [integral_finsetSum _ fun m _ ↦ (hint m).smul _]
+    simp_rw [Pi.smul_apply, integral_smul,
+      integral_stoppedValue_predictableSeqStep hd hτ hτ_ne, smul_sub]
+    have htotal : ∑ m ∈ (weight hd hs n).weights.support, (weight hd hs n).weights m = 1 := by
+      simpa [Finsupp.sum] using (weight hd hs n).total
+    rw [Finset.sum_sub_distrib, ← Finset.sum_smul, htotal, one_smul, Finsupp.sum]
+  have hMPL : Martingale (martingalePartLim hd hs) 𝓕 P := martingale_martingalePartLim hd hs
+  have h2 : ∫ ω, stoppedValue (predictablePartLim hd hs) τ ω ∂P
+      = ∫ ω, stoppedValue S τ ω ∂P - ∫ ω, S ⊥ ω ∂P := by
+    have hτ_le (ω) : τ ω ≤ ((⊤ : ι) : WithTop ι) := WithTop.le_coe_top (hτ_ne ω)
+    have hint_S : Integrable (stoppedValue S τ) P :=
+      memLp_one_iff_integrable.1 (hd.uniformIntegrable.memLp ⟨τ, hτ, hτ_ne⟩)
+    have hint_M : Integrable (stoppedValue (martingalePartLim hd hs) τ) P :=
+      hMPL.integrable_stoppedValue_of_countable_range _ hτ hτ_le hτ_count
+    rw [predictablePartLim, stoppedValue.sub]
+    simp only [Pi.sub_apply]
+    rw [integral_sub hint_S hint_M,
+      integral_congr_ae (hMPL.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ
+        hτ_le hτ_count), integral_condExp _, integral_martingalePartLim hd hs]
+  simp_rw [h1, h2]
+  exact (tendsto_weights_sum_of_forall_lt_eq_zero
+    (tendsto_integral_stoppedValue_meshCeil hd hτ hτ_ne hc)
+    fun n m hmn ↦ weight_apply_eq_zero_of_lt hd hs hmn).sub_const _
 
 /-- Reverse Fatou's lemma. See also `limsup_lintegral_le`. -/
 lemma limsup_integral_le_integral_limsup_of_tendsto_integral_posPart_sub {Ω : Type*}
@@ -1263,6 +1625,7 @@ lemma limsup_stoppedValue_predictableConvexStep_ae_eq_stoppedValue_predictablePa
     [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι] {mΩ : MeasurableSpace Ω}
     {P : Measure Ω} [IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} (hd : ClassD S 𝓕 P)
     (hs : Submartingale S 𝓕 P) {τ : Ω → WithTop ι} (hτ : IsStoppingTime 𝓕 τ)
+    (hτ_ne : ∀ ω, τ ω ≠ ⊤) (hτ_count : (Set.range τ).Countable)
     (hc : ∀ᵐ ω ∂P, IsCadlag (S · ω)) :
     limsup (fun n => stoppedValue (predictableConvexStep hd hs n) τ) atTop =ᵐ[P]
       stoppedValue (predictablePartLim hd hs) τ := by
@@ -1283,7 +1646,7 @@ lemma limsup_stoppedValue_predictableConvexStep_ae_eq_stoppedValue_predictablePa
       ∫ ω, stoppedValue (predictablePartLim hd hs) τ ω ∂P =
         limsup (fun n => ∫ ω, stoppedValue (predictableConvexStep hd hs n) τ ω ∂P) atTop :=
         ((integral_stoppedValue_predictableConvexStep_tendsto_stoppedValue_predictablePartLim
-          hd hs hτ).limsup_eq).symm
+          hd hs hτ hτ_ne hτ_count hc).limsup_eq).symm
         -- Use Fatou's lemma for the following sorry
         -- We use integral instead of lintegral because
         -- 1. `ae_eq_of_ae_le_of_lintegral_le` is the analogue of `ae_eq_of_ae_le_of_lintegral_le`,
diff --git a/BrownianMotion/StochasticIntegral/Komlos.lean b/BrownianMotion/StochasticIntegral/Komlos.lean
index d318fa68..6ca69e51 100644
--- a/BrownianMotion/StochasticIntegral/Komlos.lean
+++ b/BrownianMotion/StochasticIntegral/Komlos.lean
@@ -146,37 +146,8 @@ lemma exists_stdSimplex_of_mem_convexHull {M ι : Type*} [AddCommGroup E] [Field
     simp [aux, hw₁, hw₂]
   exact hx
 
-section
-variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-
-lemma convex_combination_bounded {x : ℕ → E}
-    {w : ℕ → StdSimplex ℝ ℕ} {M : ℝ} (hx : ∀ n, ‖x n‖ ≤ M) (n : ℕ) :
-    ‖(w n).weights.sum (fun i wi ↦ wi • x i)‖ ≤ M := by
-  have h_sum : ‖(w n).weights.sum (fun i wi => wi • x i)‖ ≤
-    ∑ i ∈ (w n).weights.support, ((w n).weights i) * ‖x i‖ := by
-    convert norm_sum_le _ _
-    · rfl
-    · rfl
-    simp [norm_smul, abs_of_nonneg ((w _).nonneg _)]
-  refine le_trans h_sum (le_trans (Finset.sum_le_sum fun i hi =>
-    mul_le_mul_of_nonneg_left (hx i) ((w n).nonneg i)) ?_)
-  rw [← Finset.sum_mul _ _ _]
-  have bound : (∑ i ∈ (w n).weights.support, (w n).weights i) ≤ 1 := by
-    rw [← (w n).total, Finsupp.sum]
-  refine mul_le_of_le_one_left ?_ bound
-  exact le_trans (norm_nonneg (x 0)) (hx 0)
-
-/-- `komlosFormula x cw k n` is the convex combination of the stage-`k` vectors `x k m`,
-weighted by `iteratedBindSimplex cw k n`. It is the sequence whose convergence is
-established at each stage of the Komlós construction. -/
-noncomputable def komlosFormula (x : ℕ → ℕ → E) (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (k i n : ℕ) : E :=
-  (StdSimplex.iteratedBind cw k n).weights.sum (fun m cwm ↦ cwm • x i m)
-
-lemma komlosFormula_congr (x : ℕ → ℕ → E) {cw1 : ℕ → ℕ → StdSimplex ℝ ℕ}
-  {cw2 : ℕ → ℕ → StdSimplex ℝ ℕ} {k : ℕ} (h : ∀ k' ≤ k, cw1 k' = cw2 k') :
-  komlosFormula x cw1 k = komlosFormula x cw2 k := by
-  unfold komlosFormula; rw [StdSimplex.iteratedBind_congr]
-  exact h
+section Module
+variable [AddCommGroup E] [Module ℝ E]
 
 /--
 We define the `convexTail` of a sequence `x` to be the set of sequences `y` with the property that
@@ -210,6 +181,40 @@ lemma exists_stdSimplex_of_mem_convexTail_reindexed {x g : ℕ → E} (hg : g 
   rw [Finsupp.sum_embDomain]
   simpa
 
+end Module
+
+section
+variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+lemma convex_combination_bounded {x : ℕ → E}
+    {w : ℕ → StdSimplex ℝ ℕ} {M : ℝ} (hx : ∀ n, ‖x n‖ ≤ M) (n : ℕ) :
+    ‖(w n).weights.sum (fun i wi ↦ wi • x i)‖ ≤ M := by
+  have h_sum : ‖(w n).weights.sum (fun i wi => wi • x i)‖ ≤
+    ∑ i ∈ (w n).weights.support, ((w n).weights i) * ‖x i‖ := by
+    convert norm_sum_le _ _
+    · rfl
+    · rfl
+    simp [norm_smul, abs_of_nonneg ((w _).nonneg _)]
+  refine le_trans h_sum (le_trans (Finset.sum_le_sum fun i hi =>
+    mul_le_mul_of_nonneg_left (hx i) ((w n).nonneg i)) ?_)
+  rw [← Finset.sum_mul _ _ _]
+  have bound : (∑ i ∈ (w n).weights.support, (w n).weights i) ≤ 1 := by
+    rw [← (w n).total, Finsupp.sum]
+  refine mul_le_of_le_one_left ?_ bound
+  exact le_trans (norm_nonneg (x 0)) (hx 0)
+
+/-- `komlosFormula x cw k n` is the convex combination of the stage-`k` vectors `x k m`,
+weighted by `iteratedBindSimplex cw k n`. It is the sequence whose convergence is
+established at each stage of the Komlós construction. -/
+noncomputable def komlosFormula (x : ℕ → ℕ → E) (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (k i n : ℕ) : E :=
+  (StdSimplex.iteratedBind cw k n).weights.sum (fun m cwm ↦ cwm • x i m)
+
+lemma komlosFormula_congr (x : ℕ → ℕ → E) {cw1 : ℕ → ℕ → StdSimplex ℝ ℕ}
+  {cw2 : ℕ → ℕ → StdSimplex ℝ ℕ} {k : ℕ} (h : ∀ k' ≤ k, cw1 k' = cw2 k') :
+  komlosFormula x cw1 k = komlosFormula x cw2 k := by
+  unfold komlosFormula; rw [StdSimplex.iteratedBind_congr]
+  exact h
+
 variable [CompleteSpace E]
 
 lemma komlos_base {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M) :
@@ -344,6 +349,18 @@ lemma Tendsto_convexTail {x : ℕ → E} {xlim : E} (hx : Tendsto x atTop (𝓝
   intro y hy
   exact TendstoUniformly.tendsto_at (TendstoUniformly_convexTail hx) ⟨y, hy⟩
 
+omit [CompleteSpace E] in
+/-- Convex combinations of a convergent sequence, given at step `n` by weights supported on
+indices at least `n`, converge to the same limit. -/
+lemma tendsto_weights_sum_of_forall_lt_eq_zero {x : ℕ → E} {xlim : E}
+    (hx : Tendsto x atTop (𝓝 xlim)) {w : ℕ → StdSimplex ℝ ℕ}
+    (hw : ∀ n, ∀ m < n, (w n).weights m = 0) :
+    Tendsto (fun n ↦ (w n).weights.sum fun m r ↦ r • x m) atTop (𝓝 xlim) := by
+  refine Tendsto_convexTail hx _ fun n ↦ ?_
+  refine Convex.sum_mem (convex_convexHull ℝ _) (fun m _ ↦ (w n).nonneg m) (w n).total
+    fun m hm ↦ subset_convexHull ℝ _ ⟨m - n, ?_⟩
+  simp [Nat.add_sub_cancel' (not_lt.1 fun h ↦ Finsupp.mem_support_iff.1 hm (hw n m h))]
+
 lemma komlos_uniform_convergence
     {x : ℕ → ℕ → E} (hx : ∀ i : ℕ, ∃ M : ℝ, ∀ n, ‖x i n‖ ≤ M)
     (cw : ℕ → ℕ → StdSimplex ℝ ℕ) (lim : ℕ → E)
@@ -446,7 +463,8 @@ private lemma cauchySeq_toLp_of_eLpNorm_approx {P : Measure Ω}
 
 theorem komlos_L1 {f : ℕ → Ω → E} {P : Measure Ω}
     [IsFiniteMeasure P] (hf : UniformIntegrable f 1 P) :
-    ∃ (g : ℕ → Ω → E) (glim : Ω → E), (∀ n, g n ∈ convexHull ℝ (Set.range fun m ↦ f (n + m))) ∧
+    ∃ (g : ℕ → Ω → E) (glim : Ω → E), MemLp glim 1 P ∧
+      (∀ n, g n ∈ convexHull ℝ (Set.range fun m ↦ f (n + m))) ∧
       Tendsto (fun n ↦ eLpNorm (g n - glim) 1 P) atTop (𝓝 0) := by
   have hbdd i : ∃ M, ∀ m, ‖(komlosTrunc_memLp i (hf.1 m)).toLp (komlosTrunc (f m) i)‖ ≤ M :=
     ⟨_, fun m ↦ komlosTrunc_norm_toLp_le i (komlosTrunc_memLp i (hf.1 m))⟩
@@ -497,7 +515,7 @@ theorem komlos_L1 {f : ℕ → Ω → E} {P : Measure Ω}
             rw [← ENNReal.ofReal_add (by positivity) (by positivity),
               show ε / 2 + ε / 2 = ε by ring]
   obtain ⟨L, hL⟩ := cauchySeq_tendsto_of_complete hcau
-  exact ⟨g, ⇑L, h_convex, ((Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ L).mp hL).congr fun n ↦
+  exact ⟨g, ⇑L, Lp.memLp L, h_convex, ((Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ L).mp hL).congr fun n ↦
     eLpNorm_congr_ae ((hgmem1 n).coeFn_toLp.sub EventuallyEq.rfl)⟩
 
 -- todo: check measurability hypothesis/conclusion