Dominated convergence of stopped-history expected nonnegative future rewards

import Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic

open MeasureTheory Filter Set
open scoped NNReal ENNReal

theorem AvramDividend.Classical.lintegral_stoppedEvent_reward_tendsto_of_bounded
    {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (A : Set Ω)
    (f : ℕ → Ω → ℝ≥0∞) (fLim : Ω → ℝ≥0∞)
    (hf : ∀ n, Measurable (Set.indicator A (f n)))
    (hlim : ∀ ω, Tendsto (fun n => f n ω) atTop (nhds (fLim ω)))
    (C : ℝ≥0∞) (hbound : ∀ n ω, f n ω ≤ C)
    (hfin : (∫⁻ _ : Ω, C ∂P) ≠ ∞) :
    Tendsto
      (fun n => ∫⁻ ω, Set.indicator A (f n) ω ∂P)
      atTop
      (nhds (∫⁻ ω, Set.indicator A fLim ω ∂P)) := by
  sorry