∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω)
  (s : ℕ → Set Ω) (n : ℕ),
  MeasureTheory.martingalePart (MeasureTheory.BorelCantelli.process s) ℱ μ n =
    ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1 | ↑ℱ k])