-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem integral_mul_upcrossingsBefore_le_integral [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hfN : ∀ ω, a ≤ f N ω) (hfzero : 0 ≤ f 0) (hab : a < b) :
    (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[f N] :=
  calc
    (b - a) * μ[upcrossingsBefore a b f N] ≤
        μ[∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)]

Proof state:
case refine_2.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
ω : Ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω

Tactic:
simpa using mul_upcrossingsBefore_le (hfN ω) hab

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ 0 ≤ᶠ[ae μ] fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)

Tactic:
exact Eventually.of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ

Tactic:
rw [← integral_mul_left]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ ∫ (a_1 : Ω), (b - a) * ↑(upcrossingsBefore a b f N a_1) ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ ∫ (a_1 : Ω), (b - a) * ↑(upcrossingsBefore a b f N a_1) ∂μ ≤
    ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ

Tactic:
refine integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_

Result:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ 0 ≤ᶠ[ae μ] fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)

case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᶠ[ae μ]
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)

Proof state:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᶠ[ae μ]
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)

Tactic:
filter_upwards with ω

Result:
case refine_2.h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
ω : Ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) ω