-- Mathlib/Probability/Martingale/Basic.lean
theorem Submartingale.sum_mul_sub [IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ}
    (hf : Submartingale f 𝒢 μ) (hξ : Adapted 𝒢 ξ) (hbdd : ∀ n ω, ξ n ω ≤ R)
    (hnonneg : ∀ n ω, 0 ≤ ξ n ω) :
    Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[ξ i * (f (i + 1) - f i)|↑𝒢 i]

Tactic:
exact EventuallyLE.trans (EventuallyLE.mul_nonneg (Eventually.of_forall (hnonneg _))
  (hf.condExp_sub_nonneg (Nat.le_succ _))) (condExp_mul_of_stronglyMeasurable_left (hξ _)
  (((hf.integrable _).sub (hf.integrable _)).bdd_mul
    hξ.stronglyMeasurable.aestronglyMeasurable (hξbdd _))
  ((hf.integrable _).sub (hf.integrable _))).symm.le

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Tactic:
refine submartingale_of_condExp_sub_nonneg_nat hadp hint fun i => ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[∑ k ∈ Finset.range (i + 1), ξ k * (f (k + 1) - f k) - ∑ k ∈ Finset.range i, ξ k * (f (k + 1) - f k)|↑𝒢 i]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
⊢ Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)

Tactic:
intro m

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
m : ℕ
⊢ StronglyMeasurable ((fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) m)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Tactic:
have hξbdd : ∀ i, ∃ C, ∀ ω, |ξ i ω| ≤ C := fun i =>
  ⟨R, fun ω => (abs_of_nonneg (hnonneg i ω)).trans_le (hbdd i ω)⟩

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
m i : ℕ
hi : i < m
⊢ StronglyMeasurable (ξ i * (f (i + 1) - f i))

Tactic:
exact (hξ.stronglyMeasurable_le hi.le).mul
  ((hf.adapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
    (hf.adapted.stronglyMeasurable_le hi.le))

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Tactic:
have hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k) := by
  intro m
  refine Finset.stronglyMeasurable_sum' _ fun i hi => ?_
  rw [Finset.mem_range] at hi
  exact (hξ.stronglyMeasurable_le hi.le).mul
    ((hf.adapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
      (hf.adapted.stronglyMeasurable_le hi.le))

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
m i : ℕ
hi : i ∈ Finset.range m
⊢ StronglyMeasurable (ξ i * (f (i + 1) - f i))

Tactic:
rw [Finset.mem_range] at hi

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : Adapted 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ C, ∀ (ω : Ω), |ξ i ω| ≤ C
hint : ∀ (m : ℕ), Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ
m i : ℕ
hi : i < m
⊢ StronglyMeasurable (ξ i * (f (i + 1) - f i))