awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n, c • μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x])
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n),
  μ[(c • f) (i + 1) - (c • f) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    c • μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: refine eventuallyEq_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ predictablePart (f + g) ℱ μ n =ᶠ[ae μ] predictablePart f ℱ μ n + predictablePart g ℱ μ n
have simp : EventuallyEq.{u_1, u_2} (β := E) (ae μ)
  (∑ i ∈ Finset.range n, μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
  (∑ x ∈ Finset.range n,
    (μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x] + μ[g (x + 1) - g x | (↑ℱ : ℕ → MeasurableSpace Ω) x]))
Tactic: simp only [predictablePart, ← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (∑ i ∈ Finset.range n, μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ x ∈ Finset.range n,
      (μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x] + μ[g (x + 1) - g x | (↑ℱ : ℕ → MeasurableSpace Ω) x]))
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n),
  μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: refine eventuallyEq_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
have simp : μ[f (i + 1) + g (i + 1) - (f i + g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
  μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) + g (i + 1) - (f i + g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
have abel_nf : μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
    (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
  μ[f (i + 1) + (g (i + 1) + (HSMul.hSMul (α := ℤ) (-1) (f i) + HSMul.hSMul (α := ℤ) (-1) (g i))) |
    (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: abel_nf
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
have _ : μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
  μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: calc
  _ =ᵐ[μ] μ[(f (i + 1) - f i) + (g (i + 1) - g i) | ℱ i] := by simp; abel_nf; rfl
  _ =ᵐ[μ] _ := by apply condExp_add ((hfint (i + 1)).sub (hfint i)) ((hgint (i + 1)).sub (hgint i))
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n i : ℕ
hi : i ∈ Finset.range n
_ :
  μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ μ[(f + g) (i + 1) - (f + g) i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
have _₁ : μ[f (i + 1) - f i + (g (i + 1) - g i) | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
  μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] + μ[g (i + 1) - g i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: calc
  _ =ᵐ[μ] μ[(f (i + 1) - f i) + (g (i + 1) - g i) | ℱ i] := by simp; abel_nf; rfl
  _ =ᵐ[μ] _ := by apply condExp_add ((hfint (i + 1)).sub (hfint i)) ((hgint (i + 1)).sub (hgint i))
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᶠ[ae μ] 0
have rw : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
  (∑ _x ∈ Finset.range n, 0)
Tactic: rw [predictablePart, ← Finset.sum_const_zero (s := Finset.range n)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ _x ∈ Finset.range n, 0)
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
Tactic: refine eventuallyEq_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
have _ : μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
  μ[f (i + 1) | (↑ℱ : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
Tactic: calc
  _ =ᵐ[μ] μ[f (i + 1) | ℱ i] - μ[f i | ℱ i] := by
    simp [condExp_sub (hf.integrable (i + 1)) (hf.integrable i) (ℱ i)]
  _ =ᵐ[μ] f i - f i := (hf.condExp_ae_eq (Nat.le_succ i)).sub (hf.condExp_ae_eq le_rfl)
  _ =ᵐ[μ] 0 := by simp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
_ :
  μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ]
    μ[f (i + 1) | (↑ℱ : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]
⊢ μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
have _₁ : f i - f i =ᶠ[ae μ] 0
Tactic: calc
  _ =ᵐ[μ] μ[f (i + 1) | ℱ i] - μ[f i | ℱ i] := by
    simp [condExp_sub (hf.integrable (i + 1)) (hf.integrable i) (ℱ i)]
  _ =ᵐ[μ] f i - f i := (hf.condExp_ae_eq (Nat.le_succ i)).sub (hf.condExp_ae_eq le_rfl)
  _ =ᵐ[μ] 0 := by simp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
have this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
Tactic: have := ae_all_iff.2 <| fun n : ℕ ↦ hf.condExp_sub_nonneg n.le_succ
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
⊢ ∀ᵐ (ω : Ω) ∂μ, Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
have h : ∀ (ω : Ω) (h : ∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω),
  Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
Tactic: filter_upwards [this] with ω h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω
⊢ Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
have h₁ : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
Tactic: simp only [Pi.zero_apply, Nat.succ_eq_add_one, ← ge_iff_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
⊢ Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
have h₁ : ∀ (n : ℕ), predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
Tactic: refine monotone_nat_of_le_succ fun n ↦ (?_ : _ ≥ _)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
n : ℕ
⊢ predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
have h₁ : (predictablePart f ℱ μ n + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ω ≥ predictablePart f ℱ μ n ω
Tactic: grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
n : ℕ
h₁ : (predictablePart f ℱ μ n + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ω ≥ predictablePart f ℱ μ n ω
⊢ predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
have h₂ : predictablePart f ℱ μ n ω + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω ≥ predictablePart f ℱ μ n ω
Tactic: grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
n : ℕ
h₁ : (predictablePart f ℱ μ n + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ω ≥ predictablePart f ℱ μ n ω
h₂ : predictablePart f ℱ μ n ω + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω ≥ predictablePart f ℱ μ n ω
⊢ predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
have h₃ : predictablePart f ℱ μ n ω + 0 ≥ predictablePart f ℱ μ n ω
Tactic: grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
ω : Ω
h : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω ≥ 0
n : ℕ
h₁ : (predictablePart f ℱ μ n + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ω ≥ predictablePart f ℱ μ n ω
h₂ : predictablePart f ℱ μ n ω + μ[f (n + 1) - f n | (↑ℱ : ℕ → MeasurableSpace Ω) n] ω ≥ predictablePart f ℱ μ n ω
h₃ : predictablePart f ℱ μ n ω + 0 ≥ predictablePart f ℱ μ n ω
⊢ predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
have h₄ : predictablePart f ℱ μ n ω ≤ predictablePart f ℱ μ n ω
Tactic: grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω
have h : ∀ (ω : Ω) (hω : Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω) (n : ℕ),
  0 ≤ predictablePart f ℱ μ n ω
Tactic: filter_upwards [hf.monotone_predictablePart] with ω hω n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᶠ[ae μ] f n - f 0
have simp : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
  (∑ i ∈ Finset.range n, (f (i + 1) - f i))
Tactic: simp only [predictablePart, ← Finset.sum_range_sub]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
c : ℝ
n : ℕ
⊢ martingalePart (c • f) ℱ μ n =ᶠ[ae μ] c • martingalePart f ℱ μ n
have h : ∀ (ω : Ω) (hω : predictablePart (c • f) ℱ μ n ω = (c • predictablePart f ℱ μ n) ω),
  martingalePart (c • f) ℱ μ n ω = (c • martingalePart f ℱ μ n) ω
Tactic: filter_upwards [predictablePart_smul (f := f) c n] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] martingalePart f ℱ μ n + martingalePart g ℱ μ n
have h : ∀ (ω : Ω) (hω : predictablePart (f + g) ℱ μ n ω = (predictablePart f ℱ μ n + predictablePart g ℱ μ n) ω),
  martingalePart (f + g) ℱ μ n ω = (martingalePart f ℱ μ n + martingalePart g ℱ μ n) ω
Tactic: filter_upwards [predictablePart_add (ℱ := ℱ) hfint hgint n] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : predictablePart (f + g) ℱ μ n ω = (predictablePart f ℱ μ n + predictablePart g ℱ μ n) ω
⊢ martingalePart (f + g) ℱ μ n ω = (martingalePart f ℱ μ n + martingalePart g ℱ μ n) ω
have h : ∀ (hω : predictablePart (f + g) ℱ μ n ω = predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω),
  f n ω + g n ω - (predictablePart f ℱ μ n ω + predictablePart g ℱ μ n ω) =
    f n ω - predictablePart f ℱ μ n ω + (g n ω - predictablePart g ℱ μ n ω)
Tactic: simp_all [martingalePart]
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
⊢ martingalePart f ℱ μ n =ᶠ[ae μ] f n
have h : ∀ (ω : Ω) (hω : predictablePart f ℱ μ n ω = 0 ω), martingalePart f ℱ μ n ω = f n ω
Tactic: filter_upwards [hf.predictablePart_eq_zero n] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ martingalePart f ℱ μ n =ᶠ[ae μ] f 0
have h : ∀ (ω : Ω) (hω : predictablePart f ℱ μ n ω = (f n - f 0) ω), martingalePart f ℱ μ n ω = f 0 ω
Tactic: filter_upwards [hf.predictablePart_eq (μ := μ) hfint n] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ martingalePart f ℱ μ = fun (n : ℕ) ↦
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
have unfold : Eq (α := ℕ → Ω → E) (fun (n : ℕ) ↦ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
  fun (n : ℕ) ↦ f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
Tactic: unfold martingalePart predictablePart
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ Eq (α := ℕ → Ω → E) (fun (n : ℕ) ↦ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    fun (n : ℕ) ↦ f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
have h : ∀ (n : ℕ),
  f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
have h : f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i) -
    ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
  f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
Tactic: rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
h :
  f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i) -
      ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
have h₁ : f 0 +
    HSub.hSub (α := Ω → E) (∑ i ∈ Finset.range n, (f (i + 1) - f i))
      (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) =
  f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
Tactic: rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
n : ℕ
h :
  f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i) -
      ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
h₁ :
  f 0 +
      HSub.hSub (α := Ω → E) (∑ i ∈ Finset.range n, (f (i + 1) - f i))
        (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]) =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
⊢ f n - ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
have h₂ : f 0 + ∑ x ∈ Finset.range n, (f (x + 1) - f x - μ[f (x + 1) - f x | (↑ℱ : ℕ → MeasurableSpace Ω) x]) =
  f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
Tactic: rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf_int : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ Integrable (martingalePart f ℱ μ n) μ
have rw : Integrable.{u_2, u_1} (ε := E)
  ((fun (n : ℕ) ↦ f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i]))
    n)
  μ
Tactic: rw [martingalePart_eq_sum]