-- Mathlib/Probability/Martingale/OptionalStopping.lean
theorem Submartingale.expected_stoppedValue_mono [SigmaFiniteFiltration μ 𝒢]
    (hf : Submartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) (hπ : IsStoppingTime 𝒢 π) (hle : τ ≤ π)
    {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) : μ[stoppedValue f τ] ≤ μ[stoppedValue f π]

Proof state:
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 ({ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) μ

Tactic:
exact Integrable.indicator (Integrable.sub (hf.integrable _) (hf.integrable _))
  (𝒢.le _ _ (this _))

Result:
no goals

Proof state:
Ω : 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 ω => (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) ω) a ∂μ

Tactic:
simp only [Finset.sum_apply]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ π : Ω → ℕ
inst✝ : SigmaFiniteFiltration μ 𝒢
hf : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
hπ : IsStoppingTime 𝒢 π
hle : τ ≤ π
N : ℕ
hbdd : ∀ (ω : Ω), π ω ≤ N
⊢ 0 ≤ ∫ (a : Ω), ∑ c ∈ Finset.range (N + 1), {ω | τ ω ≤ c ∧ c < π ω}.indicator (f (c + 1) - f c) a ∂μ

Proof state:
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 (stoppedValue f τ) μ

Tactic:
exact hf.integrable_stoppedValue hτ fun ω => le_trans (hle ω) (hbdd ω)

Result:
no goals

Proof state:
Ω : 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 < π ω}

Tactic:
intro i

Result:
Ω : 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 < π ω}

Proof state:
Ω : 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 < π ω}

Tactic:
refine (hτ i).inter ?_

Result:
Ω : 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 ω => i.succ.le (π ω)

Proof state:
Ω : 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 ω => i.succ.le (π ω)

Tactic:
convert (hπ i).compl using 1

Result:
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 ω => i.succ.le (π ω)) = {ω | π ω ≤ i}ᶜ

Proof state:
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)) (μ.restrict {ω | τ ω ≤ i ∧ i < π ω})

Tactic:
exact (hf.integrable _).integrableOn

Result:
no goals

Proof state:
Ω : 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 : Ω), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i) a ∂μ

Tactic:
rw [integral_indicator (𝒢.le _ _ (this _)), integral_sub', sub_nonneg]

Result:
Ω : 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 ∂μ

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)) (μ.restrict {ω | τ ω ≤ i ∧ i < π ω})

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) (μ.restrict {ω | τ ω ≤ i ∧ i < π ω})

Proof state:
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 ω => i + 1 ≤ π ω) ↔ i < π x

Tactic:
rfl

Result:
no goals

Proof state:
Ω : 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 ∂μ

Tactic:
exact hf.setIntegral_le (Nat.le_succ i) (this _)

Result:
no goals

Proof state:
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) (μ.restrict {ω | τ ω ≤ i ∧ i < π ω})

Tactic:
exact (hf.integrable _).integrableOn

Result:
no goals