awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hf : IsStronglyPredictable 𝒢 f
n : ℕ
⊢ f 0 ≤ᶠ[ae μ] f n

Tactic:
zero_le_of_predictable hfmgle hf.measurable_add_one n

Premises used: MeasureTheory.Submartingale.zero_le_of_predictable, MeasureTheory.IsStronglyPredictable.measurable_add_one
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : IsStronglyPredictable 𝒢 f
n : ℕ
⊢ f n ≤ᶠ[ae μ] f 0

Tactic:
le_zero_of_predictable hfmgle hfadp.measurable_add_one n

Premises used: MeasureTheory.Supermartingale.le_zero_of_predictable, MeasureTheory.IsStronglyPredictable.measurable_add_one
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : IsStronglyPredictable 𝒢 f
n : ℕ
⊢ f n =ᶠ[ae μ] f 0

Tactic:
eq_zero_of_predictable hfmgle hfadp.measurable_add_one n

Premises used: MeasureTheory.Martingale.eq_zero_of_predictable, MeasureTheory.IsStronglyPredictable.measurable_add_one
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : LE E
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
τ : Ω → ℕ∞
hτ : IsStoppingTime 𝒢 τ
N : ℕ
hbdd : ∀ (ω : Ω), τ ω ≤ (↑N : ℕ∞)
⊢ Integrable (stoppedValue f τ) μ

Tactic:
integrable_stoppedValue ℕ hτ hf.integrable hbdd

Premises used: MeasureTheory.integrable_stoppedValue, MeasureTheory.Submartingale.integrable, Nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ ∀ (i : ℕ), ∃ (C : ℝ), ∀ (ω : Ω), ‖ξ i ω‖ ≤ C

Tactic:
have hξbdd : ∀ i, ∃ C, ∀ ω, ‖ξ i ω‖ ≤ C := fun i =>
    ⟨R, fun ω => (abs_of_nonneg (hnonneg i ω)).trans_le (hbdd i ω)⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ (C : ℝ), ∀ (ω : Ω), ‖ξ i ω‖ ≤ C
choose :
  ∀ (C : (i : ℕ) → ℝ) (hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i),
    Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

Tactic:
choose C hC using hξbdd
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
⊢ ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ

Tactic:
have hint : ∀ m, Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ := fun m =>
      integrable_finsetSum' _ fun i _ => Integrable.bdd_smul
        ((hf.integrable _).sub (hf.integrable _)) (C i)
        hξ.stronglyMeasurable.aestronglyMeasurable (ae_of_all _ (hC i))
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m : ℕ
⊢ StronglyMeasurable.{u_1, u_2} (α := Ω) (β := (fun (n : ℕ) ↦ E) m)
    ((fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k) : Ω → E)) m)

Tactic:
Finset.stronglyMeasurable_sum _ fun i hi => ?_

Premises used: Finset.stronglyMeasurable_sum
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m : ℕ
refine : ∀ (i : ℕ) (hi : i ∈ Finset.range m), StronglyMeasurable (ξ i • (f (i + 1) - f i))
⊢ StronglyMeasurable.{u_1, u_2} (α := Ω) (β := (fun (n : ℕ) ↦ E) m)
    ((fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k) : Ω → E)) m)

Tactic:
refine Finset.stronglyMeasurable_sum _ fun i hi => ?_

Premises used: Finset.stronglyMeasurable_sum
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m i : ℕ
hi : i ∈ Finset.range m
⊢ i < m

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m i : ℕ
hi : i < m
⊢ StronglyMeasurable (ξ i • (f (i + 1) - f i))

Tactic:
(hξ.stronglyMeasurable_le hi.le).smul
      ((hf.stronglyAdapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
        (hf.stronglyAdapted.stronglyMeasurable_le hi.le))

Premises used: MeasureTheory.StronglyMeasurable.sub, Nat.succ_le_of_lt, MeasureTheory.StronglyMeasurable.smul, LT.lt.le, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.stronglyMeasurable_le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ 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).smul
      ((hf.stronglyAdapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
        (hf.stronglyAdapted.stronglyMeasurable_le hi.le))

Premises used: MeasureTheory.StronglyMeasurable.sub, Nat.succ_le_of_lt, MeasureTheory.StronglyMeasurable.smul, LT.lt.le, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.stronglyMeasurable_le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
⊢ StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)

Tactic:
have hadp : StronglyAdapted 𝒢 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).smul
      ((hf.stronglyAdapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
        (hf.stronglyAdapted.stronglyMeasurable_le hi.le))
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

Tactic:
submartingale_of_condExp_sub_nonneg_nat hadp hint fun i => ?_

Premises used: MeasureTheory.submartingale_of_condExp_sub_nonneg_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
refine :
  ∀ (i : ℕ),
    0 ≤ᶠ[ae μ]
      μ[HSub.hSub (α := Ω → E) (∑ k ∈ Finset.range (i + 1), ξ k • (f (k + 1) - f k))
          (∑ k ∈ Finset.range i, ξ k • (f (k + 1) - f k)) |
        (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ

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

Premises used: MeasureTheory.submartingale_of_condExp_sub_nonneg_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
simp : 0 ≤ᶠ[ae μ] μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ 0 ≤ᶠ[ae μ]
    μ[HSub.hSub (α := Ω → E) (∑ k ∈ Finset.range (i + 1), ξ k • (f (k + 1) - f k))
        (∑ k ∈ Finset.range i, ξ k • (f (k + 1) - f k)) |
      (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
simp only [← Finset.sum_Ico_eq_sub _ (Nat.le_succ _), Nat.succ_eq_add_one, Nat.Ico_succ_singleton,
    Finset.sum_singleton]

Premises used: Nat.succ_eq_add_one, Finset.sum_Ico_eq_sub, Nat.le_succ, Finset.sum_singleton, Nat.Ico_succ_singleton
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
h :
  ∀ (ω : Ω) (hω1 : 0 ω ≤ μ[f i.succ - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω)
    (hω2 :
      μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
        (ξ i • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) ω),
    0 ω ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ 0 ≤ᶠ[ae μ] μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
filter_upwards [hf.condExp_sub_nonneg i.le_succ,
    condExp_smul_of_aestronglyMeasurable_left (hξ i).aestronglyMeasurable
      (((hf.integrable (i + 1)).sub (hf.integrable i)).bdd_smul
      (C i) hξ.stronglyMeasurable.aestronglyMeasurable (ae_of_all _ (hC i)))
      ((hf.integrable _).sub (hf.integrable _))] with ω hω1 hω2

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.sub, Nat.le_succ, MeasureTheory.Integrable.bdd_smul, MeasureTheory.StronglyAdapted.stronglyMeasurable, MeasureTheory.condExp_smul_of_aestronglyMeasurable_left, HAdd.hAdd, MeasureTheory.ae_of_all, OfNat.ofNat, MeasureTheory.Submartingale.condExp_sub_nonneg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ω ≤ μ[f i.succ - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    (ξ i • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) ω
h : 0 ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ 0 ω ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω

Tactic:
simp only [Pi.zero_apply, Nat.succ_eq_add_one, Pi.smul_apply'] at hω1 hω2 ⊢

Premises used: Nat.succ_eq_add_one, Pi.smul_apply', Pi.zero_apply
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₁ : 0 ≤ ξ i ω
h₂ : LE.le.{u_2} (α := E) 0 0
⊢ 0 ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω

Tactic:
grw [← smul_zero (0 : ℝ), hnonneg i ω, hω1, hω2]

Premises used: smul_zero, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ 0 ≤ ξ i ω

Tactic:
hnonneg i ω
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ 0 ≤ ξ i ω

Tactic:
exact hnonneg i ω
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ LE.le.{u_2} (α := E) 0 0

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
ξ : ℕ → Ω → ℝ
f : ℕ → Ω → E
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (n : ℕ) ↦ ℝ) 𝒢 fun (n : ℕ) ↦ ξ (n + 1)
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ (k + 1) • (f (k + 1) - f k)) 𝒢 μ

Tactic:
hf.sum_smul_sub hξ (fun _ => hbdd _) fun _ => hnonneg _

Premises used: HAdd.hAdd, MeasureTheory.Submartingale.sum_smul_sub, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale (E := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

Tactic:
hf.sum_smul_sub hξ hbdd hnonneg

Premises used: MeasureTheory.Submartingale.sum_smul_sub
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst : IsFiniteMeasure μ
R : ℝ
ξ f : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (n : ℕ) ↦ ℝ) 𝒢 fun (n : ℕ) ↦ ξ (n + 1)
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale (E := ℝ) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ

Tactic:
hf.sum_smul_sub' hξ hbdd hnonneg

Premises used: MeasureTheory.Submartingale.sum_smul_sub'