awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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, MeasureTheory.Submartingale.stronglyMeasurable, Measurable.le, measurableSet_lt, MeasureTheory.Filtration.le, measurable_const
-- 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 ∂μ)
⊢ IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ

Tactic:
(hsub.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- 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 ∂μ)
⊢ IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
(hsub.integrable _).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- 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 ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ)

Tactic:
integral_nonneg (hnonneg _)

Premises used: MeasureTheory.integral_nonneg
-- 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 ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ)

Tactic:
integral_nonneg (hnonneg _)

Premises used: MeasureTheory.integral_nonneg
-- 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 ∂μ)
⊢ IntegrableOn (f n) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ

Tactic:
exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn,
        integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)]

Premises used: MeasureTheory.integral_nonneg, MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- 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 (∫ (ω : Ω), 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:
have hadd : ENNReal.ofReal (∫ ω, f n ω ∂μ) =
      ENNReal.ofReal
        (∫ ω in {ω | ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
          f n ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ]
        convert! rfl
        ext ω
        change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn,
        integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)]
-- 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 ∂μ)
hadd :
  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 ω ∂μ)
rwa :
  ∀
    (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 (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω}, f n ω ∂μ) +
          ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ))
    (hadd :
      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 ω ∂μ)),
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 ω ∂μ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (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 ω ∂μ))
    (hadd :
      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 ω ∂μ)),
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 ω ∂μ)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 ω ∂μ)

Tactic:
rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this

Premises used: ENNReal.add_le_add_iff_right, ENNReal.ofReal_ne_top
-- 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 : ℕ
suffices :
  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 ∂μ)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 ω ∂μ)

Tactic:
suffices ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} +
      ENNReal.ofReal
        (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
          f n ω ∂μ) ≤
      ENNReal.ofReal (μ[f n]) by
    have hadd : ENNReal.ofReal (∫ ω, f n ω ∂μ) =
      ENNReal.ofReal
        (∫ ω in {ω | ε ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
          f n ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ]
        convert! rfl
        ext ω
        change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn,
        integral_nonneg (hnonneg _), integral_nonneg (hnonneg _)]
    rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this
-- 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 : ℕ
h₁ :
  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 ℕ)) ω ∂μ)
h₂ : IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
h₃ :
  IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
h₄ : NullMeasurableSet {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
h₅ :
  ∀ (ω : Ω) (hω : Membership.mem (γ := Set Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} ω),
    f n ω ≤ 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 ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
gcongr with ω hω
-- 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 : ℕ
⊢ 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:
smul_le_stoppedValue_hittingBtwn hsub n

Premises used: MeasureTheory.smul_le_stoppedValue_hittingBtwn
-- 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 : ℕ
⊢ 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:
exact smul_le_stoppedValue_hittingBtwn hsub n

Premises used: MeasureTheory.smul_le_stoppedValue_hittingBtwn
-- 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 : ℕ
⊢ IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
(hsub.integrable n).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : ℕ
⊢ IntegrableOn (f n) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
exact (hsub.integrable n).integrableOn

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.Integrable.integrableOn
-- 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 : ℕ
⊢ IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn
-- 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 : ℕ
h₂ : Integrable (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) μ
⊢ IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
refine Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn
-- 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 : ℕ
⊢ Integrable (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) μ

Tactic:
hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue
-- 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 : ℕ
h₂ : IsStoppingTime 𝒢 fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)
⊢ Integrable (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) μ

Tactic:
refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)

Premises used: MeasureTheory.Submartingale.integrable_stoppedValue
-- 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 : ℕ
⊢ IsStoppingTime 𝒢 fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)

Tactic:
hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.Submartingale.stronglyAdapted, measurableSet_Ici
-- 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 : ℕ
⊢ IsStoppingTime 𝒢 fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)

Tactic:
exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.Submartingale.stronglyAdapted, measurableSet_Ici
-- 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 : ℕ
⊢ NullMeasurableSet {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const

Premises used: Finset.measurable_range_sup'', Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.measurable, setOf, MeasureTheory.Submartingale.stronglyMeasurable, Measurable.le, MeasureTheory.Filtration.le, nullMeasurableSet_lt, aemeasurable_const
-- 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 : ℕ
⊢ NullMeasurableSet {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ

Tactic:
exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const

Premises used: Finset.measurable_range_sup'', Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Submartingale.stronglyMeasurable, Measurable.le, MeasureTheory.Filtration.le, nullMeasurableSet_lt, aemeasurable_const
-- 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 : ℕ
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} ω
⊢ ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)

Tactic:
rw [Set.mem_setOf_eq] at hω

Premises used: Set.mem_setOf_eq
-- 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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
simp : ∀ x ∈ Set.Icc 0 n, (↑ε : ℝ) ≤ f x ω → sInf (Set.Icc 0 n ∩ {i : ℕ | (↑ε : ℝ) ≤ f i ω}) = n
⊢ hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n

Tactic:
simp only [hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, MeasureTheory.hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff
-- 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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : (↑ε : ℝ) ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i : ℕ | (↑ε : ℝ) ≤ f i ω}) = n

Tactic:
False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))

Premises used: not_le, Iff.mpr, Finset.le_sup'_iff, False.elim, Nat.lt_succ_of_le, Finset.mem_range, And.right, And.intro, Exists.intro
-- 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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : (↑ε : ℝ) ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i : ℕ | (↑ε : ℝ) ≤ f i ω}) = n

Tactic:
exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))

Premises used: not_le, Iff.mpr, Finset.le_sup'_iff, False.elim, Nat.lt_succ_of_le, Finset.mem_range, And.right, And.intro, Exists.intro
-- 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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
⊢ hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n

Tactic:
have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
-- 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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
this : hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n
h₂ : f n ω ≤ f (WithTop.untopA (↑n : WithTop ℕ)) ω
⊢ f n ω ≤ stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω

Tactic:
simp only [stoppedValue, this, ge_iff_le]

Premises used: MeasureTheory.stoppedValue, ge_iff_le