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 : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)
this : hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n
⊢ f n ω ≤ f (WithTop.untopA (↑n : WithTop ℕ)) ω

Tactic:
le_of_eq ?_

Premises used: le_of_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 ω) < (↑ε : ℝ)
this : hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n
h₂ : f n ω = f (WithTop.untopA (↑n : WithTop ℕ)) ω
⊢ f n ω ≤ f (WithTop.untopA (↑n : WithTop ℕ)) ω

Tactic:
refine le_of_eq ?_

Premises used: le_of_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 ω) < (↑ε : ℝ)
this : hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω = n
⊢ f n ω = f (WithTop.untopA (↑n : WithTop ℕ)) ω

Tactic:
congr
-- 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 : ℕ
rw :
  ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
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 (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} μ
hft :
  IntegrableOn (stoppedValue f fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ))
    {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)} μ
hp :
  LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
hq :
  LE.le (α := ℝ) 0
    (∫ (ω : Ω) 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 ℕ)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

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 : ℕ
rw :
  ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in Set.univ,
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ)
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

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 : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) 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 : ℕ
h :
  Eq.{u_1 + 1} (α := Set Ω) Set.univ
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) x ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in Set.univ,
        stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) 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 : ℕ
h :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) Set.univ ω ↔
      Membership.mem (γ := Set Ω)
        ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
          {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})
        ω
⊢ Eq.{u_1 + 1} (α := Set Ω) Set.univ
    ({ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} ∪
      {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)})

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 : ℕ
ω : Ω
⊢ Membership.mem (γ := Set Ω) Set.univ ω ↔
    ((↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) ∨ ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)

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

Tactic:
Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

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

Tactic:
exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

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

Tactic:
Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

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

Tactic:
exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))

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

Tactic:
integral_nonneg fun x => hnonneg _ _

Premises used: MeasureTheory.integral_nonneg, setOf, MeasureTheory.hittingBtwn, LE.le, Nat.cast, WithTop.untopA, OfNat.ofNat, NNReal.toReal
-- 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 : ℕ
⊢ LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
integral_nonneg fun x => hnonneg _ _

Premises used: MeasureTheory.integral_nonneg, setOf, MeasureTheory.hittingBtwn, LE.le, Nat.cast, WithTop.untopA, OfNat.ofNat, NNReal.toReal
-- 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 : ℕ
⊢ LE.le (α := ℝ) 0
    (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
      stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)

Tactic:
exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => 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 : ℕ
⊢ ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)

Tactic:
ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- 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 : ℕ
refine :
  LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)

Tactic:
refine ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- 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 : ℕ
rw :
  LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑n : WithTop ℕ)) x ∂μ)
⊢ LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), f n x ∂μ)

Tactic:
rw [← stoppedValue_const f n]

Premises used: MeasureTheory.stoppedValue_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 : ℕ
⊢ LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑n : WithTop ℕ)) x ∂μ)

Tactic:
hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)

Premises used: MeasureTheory.Adapted.isStoppingTime_hittingBtwn, MeasureTheory.StronglyAdapted.adapted, MeasureTheory.Submartingale.expected_stoppedValue_mono, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.isStoppingTime_const, 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 : ℕ
refine : ∀ (ω : Ω), (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ) ≤ (↑n : WithTop ℕ)
⊢ LE.le (α := ℝ)
    (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
    (∫ (x : Ω), stoppedValue f (fun (x : Ω) ↦ (↑n : WithTop ℕ)) x ∂μ)

Tactic:
refine hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)

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

Tactic:
simp [hittingBtwn_le]

Premises used: MeasureTheory.hittingBtwn_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
⊢ upperCrossingTime a b f N 0 = ⊥

Tactic:
rfl

Premises used: MeasureTheory.upperCrossingTime, rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
⊢ lowerCrossingTime a b f N 0 = hittingBtwn f (Set.Iic a) ⊥ N

Tactic:
rfl

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.upperCrossingTime, rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
rw rw₁ :
  (fun (ω : Ω) ↦ hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω) ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
⊢ upperCrossingTime a b f N (n + 1) ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
rw [upperCrossingTime]

Premises used: MeasureTheory.upperCrossingTime
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : OrderBot ι
inst_2 : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω =
    hittingBtwn f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
zero : upperCrossingTime a b f N 0 ω ≤ N
succ : ∀ (n : ℕ), upperCrossingTime a b f N (n + 1) ω ≤ N
⊢ upperCrossingTime a b f N n ω ≤ N

Tactic:
cases n
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
⊢ upperCrossingTime a b f N 0 ω ≤ N

Tactic:
simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]

Premises used: Pi.bot_apply, MeasureTheory.upperCrossingTime_zero, bot_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n : ℕ
⊢ upperCrossingTime a b f N (n + 1) ω ≤ N

Tactic:
simp only [upperCrossingTime_succ, hittingBtwn_le]

Premises used: MeasureTheory.hittingBtwn_le, MeasureTheory.upperCrossingTime_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f ⊥ n ω = ⊥

Tactic:
eq_bot_iff.2 upperCrossingTime_le

Premises used: Iff.mpr, MeasureTheory.upperCrossingTime_le, eq_bot_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ N

Tactic:
simp only [lowerCrossingTime, hittingBtwn_le ω]

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.hittingBtwn_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω

Tactic:
simp only [lowerCrossingTime, le_hittingBtwn upperCrossingTime_le ω]

Premises used: MeasureTheory.lowerCrossingTime, MeasureTheory.le_hittingBtwn, MeasureTheory.upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
rw :
  lowerCrossingTime a b f N n ω ≤
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
⊢ lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω

Tactic:
rw [upperCrossingTime_succ]

Premises used: MeasureTheory.upperCrossingTime_succ
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
le_hittingBtwn lowerCrossingTime_le ω

Premises used: MeasureTheory.lowerCrossingTime_le, MeasureTheory.lowerCrossingTime, MeasureTheory.le_hittingBtwn, MeasureTheory.lowerCrossingTimeAux
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
ι : Type u_2
inst : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω

Tactic:
exact le_hittingBtwn lowerCrossingTime_le ω

Premises used: MeasureTheory.lowerCrossingTime_le, MeasureTheory.le_hittingBtwn