[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
[PROOFSTEP]
rw [← sub_nonneg, ← integral_sub', stoppedValue_sub_eq_sum' hle hbdd]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ 0 ≤
    ∫ (a : Ω),
      (fun ω => Finset.sum (Finset.range (N + 1)) (fun i => Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (f (i + 1) - f i)) ω)
        a ∂μ
[PROOFSTEP]
simp only [Finset.sum_apply]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ 0 ≤ ∫ (a : Ω), Finset.sum (Finset.range (N + 1)) fun c => Set.indicator {ω | τ ω ≤ c ∧ c < π ω} (f (c + 1) - f c) a ∂μ
[PROOFSTEP]
have : ∀ i, MeasurableSet[𝒢 i] {ω : Ω | τ ω ≤ i ∧ i < π ω} :=
  by
  intro i
  refine' (hτ i).inter _
  convert (hπ i).compl using 1
  ext x
  simp; rfl
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
[PROOFSTEP]
intro i
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
⊢ MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
[PROOFSTEP]
refine' (hτ i).inter _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
⊢ MeasurableSet fun ω => Nat.le (Nat.succ i) (π ω)
[PROOFSTEP]
convert (hπ i).compl using 1
[GOAL]
case h.e'_3
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
⊢ (fun ω => Nat.le (Nat.succ i) (π ω)) = {ω | π ω ≤ i}ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
x : Ω
⊢ (x ∈ fun ω => Nat.le (Nat.succ i) (π ω)) ↔ x ∈ {ω | π ω ≤ i}ᶜ
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
i : ℕ
x : Ω
⊢ (x ∈ fun ω => Nat.succ i ≤ π ω) ↔ i < π x
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ ∫ (a : Ω), Finset.sum (Finset.range (N + 1)) fun c => Set.indicator {ω | τ ω ≤ c ∧ c < π ω} (f (c + 1) - f c) a ∂μ
[PROOFSTEP]
rw [integral_finset_sum]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ 0 ≤ Finset.sum (Finset.range (N + 1)) fun i => ∫ (a : Ω), Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (f (i + 1) - f i) a ∂μ
[PROOFSTEP]
refine' Finset.sum_nonneg fun i _ => _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ 0 ≤ ∫ (a : Ω), Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (f (i + 1) - f i) a ∂μ
[PROOFSTEP]
rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ ∫ (a : Ω) in {ω | τ ω ≤ i ∧ i < π ω}, f i a ∂μ ≤ ∫ (a : Ω) in {ω | τ ω ≤ i ∧ i < π ω}, f (i + 1) a ∂μ
[PROOFSTEP]
exact hf.set_integral_le (Nat.le_succ i) (this _)
[GOAL]
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f (i + 1))
[PROOFSTEP]
exact (hf.integrable _).integrableOn
[GOAL]
case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
x✝ : i ∈ Finset.range (N + 1)
⊢ Integrable (f i)
[PROOFSTEP]
exact (hf.integrable _).integrableOn
[GOAL]
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
⊢ ∀ (i : ℕ), i ∈ Finset.range (N + 1) → Integrable fun a => Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (f (i + 1) - f i) a
[PROOFSTEP]
intro i _
[GOAL]
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
this : ∀ (i : ℕ), MeasurableSet {ω | τ ω ≤ i ∧ i < π ω}
i : ℕ
a✝ : i ∈ Finset.range (N + 1)
⊢ Integrable fun a => Set.indicator {ω | τ ω ≤ i ∧ i < π ω} (f (i + 1) - f i) a
[PROOFSTEP]
exact Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _)) (𝒢.le _ _ (this _))
[GOAL]
case hf
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ Integrable fun x => stoppedValue f π x
[PROOFSTEP]
exact hf.integrable_stoppedValue hπ hbdd
[GOAL]
case hg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ Integrable fun x => stoppedValue f τ x
[PROOFSTEP]
exact hf.integrable_stoppedValue hτ fun ω => le_trans (hle ω) (hbdd ω)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i)
hf :
  ∀ (τ π : Ω → ℕ),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
⊢ Submartingale f 𝒢 μ
[PROOFSTEP]
refine' submartingale_of_set_integral_le hadp hint fun i j hij s hs => _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i)
hf :
  ∀ (τ π : Ω → ℕ),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
[PROOFSTEP]
classical
specialize
  hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs) (isStoppingTime_const 𝒢 j)
    (fun x => (ite_le_sup _ _ (x ∈ s)).trans (max_eq_right hij).le) ⟨j, fun _ => le_rfl⟩
rwa [stoppedValue_const, stoppedValue_piecewise_const,
  integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
  integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i)
hf :
  ∀ (τ π : Ω → ℕ),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
[PROOFSTEP]
specialize
  hf (s.piecewise (fun _ => i) fun _ => j) _ (isStoppingTime_piecewise_const hij hs) (isStoppingTime_const 𝒢 j)
    (fun x => (ite_le_sup _ _ (x ∈ s)).trans (max_eq_right hij).le) ⟨j, fun _ => le_rfl⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i)
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
hf :
  ∫ (x : Ω), stoppedValue f (Set.piecewise s (fun x => i) fun x => j) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun x => j) x ∂μ
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
[PROOFSTEP]
rwa [stoppedValue_const, stoppedValue_piecewise_const,
  integral_piecewise (𝒢.le _ _ hs) (hint _).integrableOn (hint _).integrableOn, ←
  integral_add_compl (𝒢.le _ _ hs) (hint j), add_le_add_iff_right] at hf 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ Submartingale (stoppedProcess f τ) 𝒢 μ
[PROOFSTEP]
rw [submartingale_iff_expected_stoppedValue_mono]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
[PROOFSTEP]
intro σ π hσ hπ hσ_le_π hπ_bdd
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π✝ : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ N
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
[PROOFSTEP]
simp_rw [stoppedValue_stoppedProcess]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π✝ : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ N
⊢ ∫ (x : Ω), stoppedValue f (fun ω => min (σ ω) (τ ω)) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun ω => min (π ω) (τ ω)) x ∂μ
[PROOFSTEP]
obtain ⟨n, hπ_le_n⟩ := hπ_bdd
[GOAL]
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π✝ : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue f (fun ω => min (σ ω) (τ ω)) x ∂μ ≤ ∫ (x : Ω), stoppedValue f (fun ω => min (π ω) (τ ω)) x ∂μ
[PROOFSTEP]
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 ω)
[GOAL]
case hadp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ Adapted 𝒢 (stoppedProcess f τ)
[PROOFSTEP]
exact Adapted.stoppedProcess_of_discrete h.adapted hτ
[GOAL]
case hint
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (i : ℕ), Integrable (stoppedProcess f τ i)
[PROOFSTEP]
exact fun i => h.integrable_stoppedValue ((isStoppingTime_const _ i).min hτ) fun ω => min_le_left _ _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
have hn : Set.Icc 0 n = {k | k ≤ n} := by ext x; simp
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
⊢ Set.Icc 0 n = {k | k ≤ n}
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n x : ℕ
⊢ x ∈ Set.Icc 0 n ↔ x ∈ {k | k ≤ n}
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
have :
  ∀ ω,
    ((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω) →
      (ε : ℝ) ≤ stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω :=
  by
  intro x hx
  simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx 
  refine' stoppedValue_hitting_mem _
  simp only [Set.mem_setOf_eq, exists_prop, hn]
  exact
    let ⟨j, hj₁, hj₂⟩ := hx
    ⟨j, hj₁, hj₂⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
⊢ ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
[PROOFSTEP]
intro x hx
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
x : Ω
hx : ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x
⊢ ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x
[PROOFSTEP]
simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
x : Ω
hx : ∃ b, b ≤ n ∧ ↑ε ≤ f b x
⊢ ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x
[PROOFSTEP]
refine' stoppedValue_hitting_mem _
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
x : Ω
hx : ∃ b, b ≤ n ∧ ↑ε ≤ f b x
⊢ ∃ j, j ∈ Set.Icc 0 n ∧ f j x ∈ {y | ↑ε ≤ y}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, exists_prop, hn]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
x : Ω
hx : ∃ b, b ≤ n ∧ ↑ε ≤ f b x
⊢ ∃ j, j ≤ n ∧ ↑ε ≤ f j x
[PROOFSTEP]
exact
  let ⟨j, hj₁, hj₂⟩ := hx
  ⟨j, hj₁, hj₂⟩
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
have h :=
  set_integral_ge_of_const_le
    (measurableSet_le measurable_const
      (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)))
    (measure_ne_top _ _) this
    (Integrable.integrableOn
      (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * ENNReal.toReal (↑↑μ {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a}) ≤
    ∫ (x : Ω) in {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * ENNReal.toReal (↑↑μ {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a}) ≤
    ∫ (x : Ω) in {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ ε • ENNReal.toReal (↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}) ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
[PROOFSTEP]
exact h
[GOAL]
case ha
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * ENNReal.toReal (↑↑μ {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a}) ≤
    ∫ (x : Ω) in {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≠ ⊤
[PROOFSTEP]
exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * ENNReal.toReal (↑↑μ {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a}) ≤
    ∫ (x : Ω) in {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ ↑(RingHom.id ℝ≥0∞) (↑ENNReal.ofNNRealHom ε) ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
case hb
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
hn : Set.Icc 0 n = {k | k ≤ n}
this :
  ∀ (ω : Ω),
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) →
      ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
h :
  ↑ε * ENNReal.toReal (↑↑μ {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a}) ≤
    ∫ (x : Ω) in {a | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k a},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
[PROOFSTEP]
exact le_trans (mul_nonneg ε.coe_nonneg ENNReal.toReal_nonneg) h
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ)
[PROOFSTEP]
suffices
  ε • μ {ω | (ε : ℝ) ≤ (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 ω ∂μ) ≤
    ENNReal.ofReal (μ[f n])
  by
  have hadd :
    ENNReal.ofReal (∫ ω, f n ω ∂μ) =
      ENNReal.ofReal (∫ ω in {ω | ↑ε ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω}, f n ω ∂μ) +
        ENNReal.ofReal (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_succ fun k => f k ω) < ↑ε}, f n ω ∂μ) :=
    by
    rw [← ENNReal.ofReal_add, ← integral_union]
    · rw [← integral_univ]
      convert rfl
      ext ω
      change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
      simp only [le_or_lt, Set.mem_univ]
    · rw [disjoint_iff_inf_le]
      rintro ω ⟨hω₁, hω₂⟩
      change (ε : ℝ) ≤ _ at hω₁ 
      change _ < (ε : ℝ) at hω₂ 
      exact (not_le.2 hω₂) hω₁
    ·
      exact
        measurableSet_lt (Finset.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 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ)
[PROOFSTEP]
have hadd :
  ENNReal.ofReal (∫ ω, f n ω ∂μ) =
    ENNReal.ofReal (∫ ω in {ω | ↑ε ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_succ fun k => f k ω) < ↑ε}, f n ω ∂μ) :=
  by
  rw [← ENNReal.ofReal_add, ← integral_union]
  · rw [← integral_univ]
    convert rfl
    ext ω
    change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
    simp only [le_or_lt, Set.mem_univ]
  · rw [disjoint_iff_inf_le]
    rintro ω ⟨hω₁, hω₂⟩
    change (ε : ℝ) ≤ _ at hω₁ 
    change _ < (ε : ℝ) at hω₂ 
    exact (not_le.2 hω₂) hω₁
  ·
    exact
      measurableSet_lt (Finset.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 _)]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}, f n ω ∂μ)
[PROOFSTEP]
rw [← ENNReal.ofReal_add, ← integral_union]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
      (∫ (x : Ω) in
        {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
          {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
        f n x ∂μ)
[PROOFSTEP]
rw [← integral_univ]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) 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
        {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
          {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
        f n x ∂μ)
[PROOFSTEP]
convert rfl
[GOAL]
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 : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
      {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε} =
    Set.univ
[PROOFSTEP]
ext ω
[GOAL]
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 :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
⊢ ω ∈
      {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
        {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε} ↔
    ω ∈ Set.univ
[PROOFSTEP]
change (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ) ↔ _
[GOAL]
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 :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
⊢ (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) ∨
      (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε ↔
    ω ∈ Set.univ
[PROOFSTEP]
simp only [le_or_lt, Set.mem_univ]
[GOAL]
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ Disjoint {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
    {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ⊓
      {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε} ≤
    ⊥
[PROOFSTEP]
rintro ω ⟨hω₁, hω₂⟩
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₁ : ω ∈ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
hω₂ : ω ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
⊢ ω ∈ ⊥
[PROOFSTEP]
change (ε : ℝ) ≤ _ at hω₁ 
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₂ : ω ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
hω₁ : ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω
⊢ ω ∈ ⊥
[PROOFSTEP]
change _ < (ε : ℝ) at hω₂ 
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
ω : Ω
hω₁ : ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω
hω₂ : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ ω ∈ ⊥
[PROOFSTEP]
exact (not_le.2 hω₂) hω₁
[GOAL]
case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ MeasurableSet {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
exact
  measurableSet_lt (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))
    measurable_const
[GOAL]
case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ IntegrableOn (fun ω => f n ω) {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ IntegrableOn (fun ω => f n ω) {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ 0 ≤ ∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ
case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ 0 ≤ ∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}, f n ω ∂μ
[PROOFSTEP]
exacts [(hsub.integrable _).integrableOn, (hsub.integrable _).integrableOn, integral_nonneg (hnonneg _),
  integral_nonneg (hnonneg _)]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
this :
  ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
hadd :
  ENNReal.ofReal (∫ (ω : Ω), f n ω ∂μ) =
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}, f n ω ∂μ)
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ≤
    ENNReal.ofReal
      (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}, f n ω ∂μ)
[PROOFSTEP]
rwa [hadd, ENNReal.add_le_add_iff_right ENNReal.ofReal_ne_top] at this 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
[PROOFSTEP]
calc
  ε • μ {ω | (ε : ℝ) ≤ (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 ω ∂μ) ≤
      ENNReal.ofReal
          (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_succ fun k => f k ω},
            stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ) +
        ENNReal.ofReal
          (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_succ fun k => f k ω) < ε},
            stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ) :=
    by
    refine'
      add_le_add (smul_le_stoppedValue_hitting hsub _)
        (ENNReal.ofReal_le_ofReal
          (set_integral_mono_on (hsub.integrable n).integrableOn
            (Integrable.integrableOn
              (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))
            (measurableSet_lt
              (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))
              measurable_const)
            _))
    intro ω hω
    rw [Set.mem_setOf_eq] at hω 
    have : hitting f {y : ℝ | ↑ε ≤ y} 0 n ω = n :=
      by
      classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.coe_nat, Nat.cast_id, 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⟩))
    simp_rw [stoppedValue, this, le_rfl]
  _ = ENNReal.ofReal (∫ ω, stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ) :=
    by
    rw [← ENNReal.ofReal_add, ← integral_union]
    · rw [← integral_univ (μ := μ)]
      convert rfl
      ext ω
      change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)
      simp only [le_or_lt, Set.mem_univ]
    · rw [disjoint_iff_inf_le]
      rintro ω ⟨hω₁, hω₂⟩
      change (ε : ℝ) ≤ _ at hω₁ 
      change _ < (ε : ℝ) at hω₂ 
      exact (not_le.2 hω₂) hω₁
    ·
      exact
        measurableSet_lt (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))
          measurable_const
    ·
      exact
        Integrable.integrableOn
          (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)
    ·
      exact
        Integrable.integrableOn
          (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)
    exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => hnonneg _ _]
  _ ≤ ENNReal.ofReal (μ[f n]) := by
    refine' ENNReal.ofReal_le_ofReal _
    rw [← stoppedValue_const f n]
    exact
      hsub.expected_stoppedValue_mono (hitting_isStoppingTime hsub.adapted measurableSet_Ici) (isStoppingTime_const _ _)
        (fun ω => hitting_le ω) (fun _ => le_rfl : ∀ _, n ≤ n)
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ε • ↑↑μ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          f n ω ∂μ) ≤
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
refine'
  add_le_add (smul_le_stoppedValue_hitting hsub _)
    (ENNReal.ofReal_le_ofReal
      (set_integral_mono_on (hsub.integrable n).integrableOn
        (Integrable.integrableOn
          (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))
        (measurableSet_lt (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))
          measurable_const)
        _))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ∀ (x : Ω),
    x ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε} →
      f n x ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x
[PROOFSTEP]
intro ω hω
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ω ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
[PROOFSTEP]
rw [Set.mem_setOf_eq] at hω 
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
[PROOFSTEP]
have : hitting f {y : ℝ | ↑ε ≤ y} 0 n ω = n :=
  by
  classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.coe_nat, Nat.cast_id, 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⟩))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ hitting f {y | ↑ε ≤ y} 0 n ω = n
[PROOFSTEP]
classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.coe_nat, Nat.cast_id, ite_eq_right_iff,
  forall_exists_index, and_imp]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ hitting f {y | ↑ε ≤ y} 0 n ω = n
[PROOFSTEP]
simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.coe_nat, Nat.cast_id, ite_eq_right_iff, forall_exists_index,
  and_imp]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ ∀ (x : ℕ), x ∈ Set.Icc 0 n → ↑ε ≤ f x ω → sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n
[PROOFSTEP]
intro m hm hεm
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
m : ℕ
hm : m ∈ Set.Icc 0 n
hεm : ↑ε ≤ f m ω
⊢ sInf (Set.Icc 0 n ∩ {i | ↑ε ≤ f i ω}) = n
[PROOFSTEP]
exact False.elim ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
this : hitting f {y | ↑ε ≤ y} 0 n ω = n
⊢ f n ω ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω
[PROOFSTEP]
simp_rw [stoppedValue, this, le_rfl]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
        (∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
          stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
rw [← ENNReal.ofReal_add, ← integral_union]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
          {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
        stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ) =
    ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
[PROOFSTEP]
rw [← integral_univ (μ := μ)]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal
      (∫ (x : Ω) in
        {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
          {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) 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 ∂μ)
[PROOFSTEP]
convert rfl
[GOAL]
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 =
    {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
      {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
ext ω
[GOAL]
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 ↔
    ω ∈
      {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ∪
        {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)
[GOAL]
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 ↔
    (↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) ∨
      (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
[PROOFSTEP]
simp only [le_or_lt, Set.mem_univ]
[GOAL]
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ Disjoint {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
    {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case hst
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω} ⊓
      {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε} ≤
    ⊥
[PROOFSTEP]
rintro ω ⟨hω₁, hω₂⟩
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₁ : ω ∈ {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
hω₂ : ω ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
⊢ ω ∈ ⊥
[PROOFSTEP]
change (ε : ℝ) ≤ _ at hω₁ 
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₂ : ω ∈ {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
hω₁ : ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω
⊢ ω ∈ ⊥
[PROOFSTEP]
change _ < (ε : ℝ) at hω₂ 
[GOAL]
case hst.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω₁ : ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω
hω₂ : (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε
⊢ ω ∈ ⊥
[PROOFSTEP]
exact (not_le.2 hω₂) hω₁
[GOAL]
case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ MeasurableSet {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
exact
  measurableSet_lt (Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n))
    measurable_const
[GOAL]
case hfs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (fun ω => stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω)
    {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω}
[PROOFSTEP]
exact
  Integrable.integrableOn
    (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)
[GOAL]
case hft
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ IntegrableOn (fun ω => stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω)
    {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε}
[PROOFSTEP]
exact
  Integrable.integrableOn
    (hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le)
[GOAL]
case hp
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | ↑ε ≤ sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
case hq
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ 0 ≤
    ∫ (ω : Ω) in {ω | (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k ω) < ↑ε},
      stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
[PROOFSTEP]
exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => hnonneg _ _]
[GOAL]
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (∫ (ω : Ω), stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ) ≤ ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
[PROOFSTEP]
refine' ENNReal.ofReal_le_ofReal _
[GOAL]
Ω : 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 : Ω), f n x ∂μ
[PROOFSTEP]
rw [← stoppedValue_const f n]
[GOAL]
Ω : 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 ∂μ
[PROOFSTEP]
exact
  hsub.expected_stoppedValue_mono (hitting_isStoppingTime hsub.adapted measurableSet_Ici) (isStoppingTime_const _ _)
    (fun ω => hitting_le ω) (fun _ => le_rfl : ∀ _, n ≤ n)
