awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have hhdef : let h := f - martingalePart (f + g) ℱ μ;
h = f - martingalePart (f + g) ℱ μ
Tactic: set h := f - martingalePart (f + g) ℱ μ with hhdef
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
rw : f - martingalePart (f + g) ℱ μ = predictablePart (f + g) ℱ μ - g
⊢ h = predictablePart (f + g) ℱ μ - g
have rw₁ : f + g = predictablePart (f + g) ℱ μ + martingalePart (f + g) ℱ μ
Tactic: rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
rw : f - martingalePart (f + g) ℱ μ = predictablePart (f + g) ℱ μ - g
rw₁ : f + g = predictablePart (f + g) ℱ μ + martingalePart (f + g) ℱ μ
⊢ h = predictablePart (f + g) ℱ μ - g
have rw₂ : f + g = martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ
Tactic: rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
rw : f - martingalePart (f + g) ℱ μ = predictablePart (f + g) ℱ μ - g
rw₁ : f + g = predictablePart (f + g) ℱ μ + martingalePart (f + g) ℱ μ
rw₂ : f + g = martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ
⊢ h = predictablePart (f + g) ℱ μ - g
have rw₃ : f + g = f + g
Tactic: rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_predictablePart]
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have hh : h = predictablePart (f + g) ℱ μ - g
Tactic: have hh : h = predictablePart (f + g) ℱ μ - g := by
    rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
⊢ StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
have rw : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ (predictablePart (f + g) ℱ μ - g) (n + 1)
Tactic: rw [hh]
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
Tactic: have hhpred : StronglyAdapted ℱ fun n => h (n + 1) := by
    rw [hh]
    exact stronglyAdapted_predictablePart.sub hg
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have this : IsStronglyPredictable ℱ g
Tactic: have := (IsStronglyPredictable.of_measurable_add_one (hg0.symm ▸ stronglyMeasurable_zero) hg)
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have hhmgle : Martingale h ℱ μ
Tactic: have hhmgle : Martingale h ℱ μ := hf.sub (martingale_martingalePart
    (hf.stronglyAdapted.add this.stronglyAdapted) fun n => (hf.integrable n).add <| hgint 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
have refine : f n - martingalePart (f + g) ℱ μ n =ᶠ[ae μ] 0
Tactic: refine (eventuallyEq_iff_sub.2 ?_).symm
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
⊢ f n - martingalePart (f + g) ℱ μ n =ᶠ[ae μ] 0
have h₁ : ∀ (ω : Ω) (hω : h n ω = h 0 ω), (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
Tactic: filter_upwards [hhmgle.eq_zero_of_predictable hhpred n] 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f - martingalePart (f + g) ℱ μ) n ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
have hω₁ : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
Tactic: rw [Pi.sub_apply] 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
hh : h = predictablePart (f + g) ℱ μ - g
hhpred : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)
this : IsStronglyPredictable ℱ g
hhmgle : Martingale h ℱ μ
ω : Ω
hω : (f n - martingalePart (f + g) ℱ μ n) ω = (f - martingalePart (f + g) ℱ μ) 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
have h₁ : (f 0 - ((f + g) 0 - predictablePart (f + g) ℱ μ 0)) ω = 0 ω
Tactic: rw [hω, Pi.sub_apply, martingalePart]
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ predictablePart (f + g) ℱ μ n =ᶠ[ae μ] g n
have h : ∀ (ω : Ω) (hω : martingalePart (f + g) ℱ μ n ω = f n ω), predictablePart (f + g) ℱ μ n ω = g n ω
Tactic: filter_upwards [martingalePart_add_ae_eq hf hg hg0 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ predictablePart (f + g) ℱ μ n ω = g n ω
have h : f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω
Tactic: rw [← add_right_inj (f 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
| f n ω + g n ω
have rw : (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
Tactic: rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω
have h : f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
Tactic: conv_rhs => rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]
-- 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
have h : f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ n + predictablePart (f + g) ℱ μ n) ω
Tactic: rw [Pi.add_apply, Pi.add_apply, 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
h : f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ n + predictablePart (f + g) ℱ μ n) ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
have h₁ : f n ω + predictablePart (f + g) ℱ μ n ω = martingalePart (f + g) ℱ μ n ω + predictablePart (f + g) ℱ μ n ω
Tactic: rw [Pi.add_apply, Pi.add_apply, 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
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
ω : Ω
hω : martingalePart (f + g) ℱ μ n ω = f n ω
h : f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ n + predictablePart (f + g) ℱ μ n) ω
h₁ : f n ω + predictablePart (f + g) ℱ μ n ω = martingalePart (f + g) ℱ μ n ω + predictablePart (f + g) ℱ μ n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
have h₂ : f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + predictablePart (f + g) ℱ μ n ω
Tactic: rw [Pi.add_apply, Pi.add_apply, hω]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)
have simp_rw : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω| ≤ (↑R : ℝ)
Tactic: simp_rw [predictablePart, Finset.sum_apply, Finset.sum_range_succ_sub_sum]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ (↑(2 * R) : ℝ)
have h : ∀ (ω : Ω) (hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ))
  (hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)) (i : ℕ),
  |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ (↑(2 * R) : ℝ)
Tactic: filter_upwards [hbdd, predictablePart_bdd_difference ℱ hbdd] with ω hω₁ hω₂ i
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ω : Ω
hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ (↑(2 * R) : ℝ)
have h : |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
Tactic: simp only [two_mul, martingalePart, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ω : Ω
hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
have this : |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| =
  |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)|
Tactic: have : |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| =
      |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| := by
    ring_nf
-- Lean 4 proof step from Mathlib.Probability.Martingale.Centering (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ω : Ω
hω₁ : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
hω₂ : ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)
i : ℕ
this :
  |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| =
    |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)|
⊢ |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
have h : |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : upcrossings a b f ω ≠ ∞
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
have hω₁ : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Tactic: rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
have obtain : ∀ (k : ℕ) (hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k), ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
Tactic: obtain ⟨k, hk⟩ := hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
have hω₁ : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
Tactic: replace hω : ∃ k, ∀ N, upcrossingsBefore a b f N ω < k := by
    obtain ⟨k, hk⟩ := hω
    exact ⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
⊢ False
have h₃ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
Tactic: rw [frequently_atTop] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
h₃ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
⊢ False
have h₄ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
Tactic: rw [frequently_atTop] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
⊢ False
have refine : ¬∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
Tactic: refine Classical.not_not.2 hω ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
⊢ ¬∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
have push : ∀ (k : ℕ), ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω
Tactic: push Not
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k : ℕ
ih : ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
have succ : ∀ (N : ℕ) (hN : k ≤ upcrossingsBefore a b f N ω), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
Tactic: obtain ⟨N, hN⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
have succ : ∀ (N₁ : ℕ) (hN₁ : N₁ ≥ N) (hN₁' : f N₁ ω < a), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
Tactic: obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N