-- Mathlib/Probability/Martingale/Basic.lean
theorem Submartingale.condExp_sub_nonneg {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) {i j : ι}
    (hij : i ≤ j) : 0 ≤ᵐ[μ] μ[f j - f i|ℱ i]

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]

Tactic:
rw [eventually_sub_nonneg,
  condExp_of_stronglyMeasurable (ℱ.le _) (hf.adapted _) (hf.integrable _)]

Result:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]

Proof state:
case neg
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Tactic:
rw [condExp_of_not_sigmaFinite (ℱ.le i) h]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Tactic:
by_cases h : SigmaFinite (μ.trim (ℱ.le i))

Result:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

case neg
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]

Tactic:
exact hf.2.1 i j hij

Result:
no goals

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

case neg
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Tactic:
swap

Result:
case neg
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Proof state:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

Tactic:
refine EventuallyLE.trans ?_ (condExp_sub (hf.integrable _) (hf.integrable _) _).symm.le

Result:
case pos
Ω : Type u_1
ι : Type u_3
inst✝ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
f : ι → Ω → ℝ
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]