-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnonneg : 0 ≤ f) {ε : ℝ≥0}
    (n : ℕ) : ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω} ≤
    ENNReal.ofReal (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω},
      f n ω ∂μ)

Proof state:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      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 ω) < ↑ε} ≤ ⊥

Tactic:
rintro ω ⟨hω₁, hω₂⟩

Result:
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₁ : ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}
hω₂ : ω ∈ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}
⊢ ω ∈ ⊥

Proof state:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      ENNReal.ofReal (∫ (ω : Ω) in {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ Disjoint {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

Tactic:
rw [disjoint_iff_inf_le]

Result:
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      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 ω) < ↑ε} ≤ ⊥

Proof state:
case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n)) {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε} μ

Tactic:
exact Integrable.integrableOn (hsub.integrable_stoppedValue
  (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)

Result:
no goals

Proof state:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Set.univ = {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

Tactic:
ext ω

Result:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔
    ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

Proof state:
Ω : 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 ω) < ↑ε
⊢ hitting f {y | ↑ε ≤ y} 0 n ω = n

Tactic:
classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.natCast_def, Nat.cast_id,
  ite_eq_right_iff, forall_exists_index, and_imp]

Result:
Ω : 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 ω) < ↑ε
⊢ ∀ x ∈ Set.Icc 0 n, ↑ε ≤ f x ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x => n) x ∂μ

Tactic:
exact hsub.expected_stoppedValue_mono (hitting_isStoppingTime hsub.adapted measurableSet_Ici)
  (isStoppingTime_const _ _) (fun ω => hitting_le ω) (fun _ => le_refl n)

Result:
no goals

Proof state:
Ω : 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 (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)

Tactic:
rw [← setIntegral_univ (μ := μ)]

Result:
Ω : 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 (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ) =
    ENNReal.ofReal (∫ (x : Ω) in Set.univ, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ)

Proof state:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} +
      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 ω) < ↑ε ↔ ω ∈ Set.univ

Tactic:
simp only [le_or_lt, Set.mem_univ]

Result:
no goals

Proof state:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔ (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) ∨ ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε

Tactic:
simp only [le_or_lt, Set.mem_univ]

Result:
no goals

Proof state:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔
    ω ∈ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ∪ {ω | ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε}

Tactic:
change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)

Result:
case h.e'_3.h.e'_1.h.e'_6.h.e'_4.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
⊢ ω ∈ Set.univ ↔ (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) ∨ ((range (n + 1)).sup' ⋯ fun k => f k ω) < ↑ε