awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hσ_top : ∀ (ω : Ω), σ ω ≠ ⊤
⊢ LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x ∂μ)

Tactic:
h.expected_stoppedValue_mono (hσ.min hτ) (hπ.min hτ)
      (fun ω => min_le_min (hσ_le_π ω) le_rfl) fun ω => (min_le_left _ _).trans (hπ_le_n ω)

Premises used: le_rfl, MeasureTheory.IsStoppingTime.min, MeasureTheory.Submartingale.expected_stoppedValue_mono, min_le_left, LE.le.trans, min_le_min
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ (↑n : ℕ∞)
hπ_top : ∀ (ω : Ω), π ω ≠ ⊤
hσ_top : ∀ (ω : Ω), σ ω ≠ ⊤
⊢ LE.le (α := ℝ) (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (σ ω) (τ ω)) x ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (ω : Ω) ↦ min (π ω) (τ ω)) x ∂μ)

Tactic:
exact h.expected_stoppedValue_mono (hσ.min hτ) (hπ.min hτ)
      (fun ω => min_le_min (hσ_le_π ω) le_rfl) fun ω => (min_le_left _ _).trans (hπ_le_n ω)

Premises used: le_rfl, MeasureTheory.IsStoppingTime.min, MeasureTheory.Submartingale.expected_stoppedValue_mono, min_le_left, LE.le.trans, min_le_min
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 (stoppedProcess f τ)

Tactic:
StronglyAdapted.stoppedProcess_of_discrete h.stronglyAdapted hτ

Premises used: MeasureTheory.StronglyAdapted.stoppedProcess_of_discrete, MeasureTheory.Submartingale.stronglyAdapted
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 (stoppedProcess f τ)

Tactic:
exact StronglyAdapted.stoppedProcess_of_discrete h.stronglyAdapted hτ

Premises used: MeasureTheory.StronglyAdapted.stoppedProcess_of_discrete, MeasureTheory.Submartingale.stronglyAdapted
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ

Tactic:
fun i =>
      h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _

Premises used: MeasureTheory.stoppedValue, MeasureTheory.IsStoppingTime.min, MeasureTheory.stoppedProcess, WithTop.some, min_le_left, MeasureTheory.isStoppingTime_const, MeasureTheory.Submartingale.integrable_stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ

Tactic:
exact fun i =>
      h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _

Premises used: MeasureTheory.IsStoppingTime.min, WithTop.some, min_le_left, MeasureTheory.isStoppingTime_const, MeasureTheory.Submartingale.integrable_stoppedValue
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x
⊢ ∃ b ≤ n, (↑ε : ℝ) ≤ f b x

Tactic:
simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx

Premises used: Finset.le_sup'_iff, Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
⊢ (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x

Tactic:
stoppedValue_hittingBtwn_mem ?_

Premises used: Set.Mem, MeasureTheory.stoppedValue_hittingBtwn_mem
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
refine : ∃ j ∈ Set.Icc 0 n, Membership.mem (γ := Set ℝ) {y : ℝ | (↑ε : ℝ) ≤ y} (f j x)
⊢ (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x

Tactic:
refine stoppedValue_hittingBtwn_mem ?_

Premises used: MeasureTheory.stoppedValue_hittingBtwn_mem
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
simp : ∃ j ≤ n, (↑ε : ℝ) ≤ f j x
⊢ ∃ j ∈ Set.Icc 0 n, Membership.mem (γ := Set ℝ) {y : ℝ | (↑ε : ℝ) ≤ y} (f j x)

Tactic:
simp only [Set.mem_Icc, zero_le, true_and, Set.mem_setOf_eq]

Premises used: zero_le, Set.mem_setOf_eq, Set.mem_Icc, true_and
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
⊢ ∃ j ≤ n, (↑ε : ℝ) ≤ f j x

Tactic:
let ⟨j, hj₁, hj₂⟩ := hx
      ⟨j, hj₁, hj₂⟩

Premises used: Exists, LE.le, And, And.intro, Exists.intro, _private.0.MeasureTheory.smul_le_stoppedValue_hittingBtwn.match_5, NNReal.toReal
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, (↑ε : ℝ) ≤ f b x
⊢ ∃ j ≤ n, (↑ε : ℝ) ≤ f j x

Tactic:
exact
      let ⟨j, hj₁, hj₂⟩ := hx
      ⟨j, hj₁, hj₂⟩
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
⊢ ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω

Tactic:
have : ∀ ω, ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) →
      (ε : ℝ) ≤ stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω := by
    intro x hx
    simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx
    refine stoppedValue_hittingBtwn_mem ?_
    simp only [Set.mem_Icc, zero_le, true_and, Set.mem_setOf_eq]
    exact
      let ⟨j, hj₁, hj₂⟩ := hx
      ⟨j, hj₁, hj₂⟩
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
⊢ (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ

Tactic:
have h := setIntegral_ge_of_const_le_real (measurableSet_le measurable_const
    (measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)))
      (measure_ne_top _ _) this (Integrable.integrableOn (hsub.integrable_stoppedValue
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (mod_cast hittingBtwn_le)))
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
rw :
  ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}) ≤
    ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ
ha :
  HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≠
    ∞
hb :
  LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]

Premises used: ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}) ≤
    ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ

Tactic:
h

Premises used: setOf, MeasureTheory.Measure.real
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ ε • ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}) ≤
    ∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ

Tactic:
exact h
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ (↑ε : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
      ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) ≠
    ∞

Tactic:
exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)

Premises used: MeasureTheory.measure_ne_top, ENNReal.mul_ne_top
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
le_trans (mul_nonneg ε.coe_nonneg ENNReal.toReal_nonneg) h

Premises used: mul_nonneg, ENNReal.toReal_nonneg, NNReal.coe_nonneg, le_trans
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
this :
  ∀ (ω : Ω),
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) →
      (↑ε : ℝ) ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω
h :
  (↑ε : ℝ) * μ.real {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a} ≤
    ∫ (x : Ω) in {a : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k a},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ
⊢ LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
exact le_trans (mul_nonneg ε.coe_nonneg ENNReal.toReal_nonneg) h

Premises used: mul_nonneg, ENNReal.toReal_nonneg, NNReal.coe_nonneg, le_trans
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
hst :
  Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
ht : MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}
hfs : IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
hft : IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
hp : LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)
hq : LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)

Tactic:
rw [← ENNReal.ofReal_add, ← setIntegral_union]

Premises used: MeasureTheory.setIntegral_union, ENNReal.ofReal_add
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
rw :
  ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)

Tactic:
rw [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ) = ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
h :
  Eq.{u_1 + 1} (α := Set Ω)
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
    Set.univ
⊢ ENNReal.ofReal (∫ (x : Ω) in Set.univ, f n x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        f n x ∂μ)

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω)
        ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
        ω ↔
      Membership.mem (γ := Set Ω) Set.univ ω
⊢ Eq.{u_1 + 1} (α := Set Ω)
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
    Set.univ

Tactic:
ext ω
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
⊢ ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) ∨ ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ) ↔
    Membership.mem (γ := Set Ω) Set.univ ω

Tactic:
simp only [le_or_gt, Set.mem_univ]

Premises used: le_or_gt, Set.mem_univ
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ Disjoint.{u_1} (α := Set Ω) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}

Tactic:
grind
-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ MeasurableSet.{u_1} (α := Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}

Tactic:
measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const

Premises used: Finset.measurable_range_sup'', MeasureTheory.StronglyMeasurable.measurable, setOf, MeasureTheory.Submartingale.stronglyMeasurable, Measurable.le, measurableSet_lt, MeasureTheory.Filtration.le, measurable_const