awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Centering
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.{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:
fun_prop
-- Module: Mathlib.Probability.Martingale.Centering
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 : ℕ
⊢ let h := f - martingalePart (f + g) ℱ μ;
  h = f - martingalePart (f + g) ℱ μ

Tactic:
set h := f - martingalePart (f + g) ℱ μ with hhdef

Premises used: MeasureTheory.martingalePart, HAdd.hAdd
-- Module: Mathlib.Probability.Martingale.Centering
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) ℱ μ
rw₃ rw₄ : f + g = f + g
⊢ h = predictablePart (f + g) ℱ μ - g

Tactic:
rw [hhdef, sub_eq_sub_iff_add_eq_add, add_comm (predictablePart (f + g) ℱ μ),
      martingalePart_add_predictablePart]

Premises used: sub_eq_sub_iff_add_eq_add, add_comm, MeasureTheory.martingalePart_add_predictablePart, HAdd.hAdd, MeasureTheory.predictablePart
-- Module: Mathlib.Probability.Martingale.Centering
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) ℱ μ
⊢ 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]
-- Module: Mathlib.Probability.Martingale.Centering
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
rw : StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ (predictablePart (f + g) ℱ μ - g) (n + 1)
⊢ StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ h (n + 1)

Tactic:
rw [hh]
-- Module: Mathlib.Probability.Martingale.Centering
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 : ℕ) ↦ (predictablePart (f + g) ℱ μ - g) (n + 1)

Tactic:
stronglyAdapted_predictablePart.sub hg

Premises used: MeasureTheory.StronglyAdapted.sub, MeasureTheory.stronglyAdapted_predictablePart
-- Module: Mathlib.Probability.Martingale.Centering
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 : ℕ) ↦ (predictablePart (f + g) ℱ μ - g) (n + 1)

Tactic:
exact stronglyAdapted_predictablePart.sub hg

Premises used: MeasureTheory.StronglyAdapted.sub, MeasureTheory.stronglyAdapted_predictablePart
-- Module: Mathlib.Probability.Martingale.Centering
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)

Tactic:
have hhpred : StronglyAdapted ℱ fun n => h (n + 1) := by
    rw [hh]
    exact stronglyAdapted_predictablePart.sub hg
-- Module: Mathlib.Probability.Martingale.Centering
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)
⊢ IsStronglyPredictable ℱ g

Tactic:
have := (IsStronglyPredictable.of_measurable_add_one (hg0.symm ▸ stronglyMeasurable_zero) hg)
-- Module: Mathlib.Probability.Martingale.Centering
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
⊢ Martingale h ℱ μ

Tactic:
have hhmgle : Martingale h ℱ μ := hf.sub (martingale_martingalePart
    (hf.stronglyAdapted.add this.stronglyAdapted) fun n => (hf.integrable n).add <| hgint n)
-- Module: Mathlib.Probability.Martingale.Centering
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

Tactic:
(eventuallyEq_iff_sub.2 ?_).symm

Premises used: Iff.mpr, Filter.eventuallyEq_iff_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Centering
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 ℱ μ
refine : f n - martingalePart (f + g) ℱ μ n =ᶠ[ae μ] 0
⊢ martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n

Tactic:
refine (eventuallyEq_iff_sub.2 ?_).symm

Premises used: Iff.mpr, Filter.eventuallyEq_iff_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Centering
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₁ : ∀ (ω : Ω) (hω : h n ω = h 0 ω), (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω
⊢ f n - martingalePart (f + g) ℱ μ n =ᶠ[ae μ] 0

Tactic:
filter_upwards [hhmgle.eq_zero_of_predictable hhpred n] with ω hω

Premises used: MeasureTheory.Martingale.eq_zero_of_predictable
-- Module: Mathlib.Probability.Martingale.Centering
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) ω = (f - martingalePart (f + g) ℱ μ) 0 ω

Tactic:
rw [Pi.sub_apply] at hω

Premises used: Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Centering
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 ω
h₁ : (f 0 - ((f + g) 0 - predictablePart (f + g) ℱ μ 0)) ω = 0 ω
⊢ (f n - martingalePart (f + g) ℱ μ n) ω = 0 ω

Tactic:
rw [hω, Pi.sub_apply, martingalePart]

Premises used: MeasureTheory.martingalePart, Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Centering
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 0 - ((f + g) 0 - predictablePart (f + g) ℱ μ 0)) ω = 0 ω

Tactic:
simp [hg0]
-- Module: Mathlib.Probability.Martingale.Centering
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 : ∀ (ω : Ω) (hω : martingalePart (f + g) ℱ μ n ω = f n ω), predictablePart (f + g) ℱ μ n ω = g n ω
⊢ predictablePart (f + g) ℱ μ n =ᶠ[ae μ] g n

Tactic:
filter_upwards [martingalePart_add_ae_eq hf hg hg0 hgint n] with ω hω

Premises used: MeasureTheory.martingalePart_add_ae_eq
-- Module: Mathlib.Probability.Martingale.Centering
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 ω = f n ω + g n ω
⊢ predictablePart (f + g) ℱ μ n ω = g n ω

Tactic:
rw [← add_right_inj (f n ω)]

Premises used: add_right_inj
-- Module: Mathlib.Probability.Martingale.Centering
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 ω
rw : (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω
| f n ω + g n ω

Tactic:
rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]

Premises used: MeasureTheory.martingalePart_add_predictablePart, Pi.add_apply, HAdd.hAdd
-- Module: Mathlib.Probability.Martingale.Centering
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) ℱ μ + predictablePart (f + g) ℱ μ) n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + g n ω

Tactic:
conv_rhs => rw [← Pi.add_apply, ← Pi.add_apply, ← martingalePart_add_predictablePart ℱ μ (f + g)]

Premises used: MeasureTheory.martingalePart_add_predictablePart, Pi.add_apply, HAdd.hAdd
-- Module: Mathlib.Probability.Martingale.Centering
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 ω
h₂ h₃ : f n ω + predictablePart (f + g) ℱ μ n ω = f n ω + predictablePart (f + g) ℱ μ n ω
⊢ f n ω + predictablePart (f + g) ℱ μ n ω = (martingalePart (f + g) ℱ μ + predictablePart (f + g) ℱ μ) n ω

Tactic:
rw [Pi.add_apply, Pi.add_apply, hω]

Premises used: Pi.add_apply
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
simp_rw : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ (↑R : ℝ)

Tactic:
simp_rw [predictablePart, Finset.sum_apply, Finset.sum_range_succ_sub_sum]

Premises used: Finset.sum_apply, MeasureTheory.predictablePart, Finset.sum_range_succ_sub_sum
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω| ≤ (↑R : ℝ)

Tactic:
ae_all_iff.2 fun i => ae_bdd_condExp_of_ae_bdd <| ae_all_iff.1 hbdd i

Premises used: Iff.mpr, MeasureTheory.ae_bdd_condExp_of_ae_bdd, Iff.mp, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω| ≤ (↑R : ℝ)

Tactic:
exact ae_all_iff.2 fun i => ae_bdd_condExp_of_ae_bdd <| ae_all_iff.1 hbdd i

Premises used: Iff.mpr, MeasureTheory.ae_bdd_condExp_of_ae_bdd, Iff.mp, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
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) : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ (↑(2 * R) : ℝ)

Tactic:
filter_upwards [hbdd, predictablePart_bdd_difference ℱ hbdd] with ω hω₁ hω₂ i

Premises used: MeasureTheory.predictablePart_bdd_difference
-- Module: Mathlib.Probability.Martingale.Centering
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 : ℕ
h : |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
⊢ |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ (↑(2 * R) : ℝ)

Tactic:
simp only [two_mul, martingalePart, Pi.sub_apply]

Premises used: MeasureTheory.martingalePart, two_mul, Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Centering
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 ω)| =
    |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)|

Tactic:
ring_nf
-- Module: Mathlib.Probability.Martingale.Centering
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 ω)| =
    |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
-- Module: Mathlib.Probability.Martingale.Centering
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 ω)|
h : |f (i + 1) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)
⊢ |f (i + 1) ω - predictablePart f ℱ μ (i + 1) ω - (f i ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Martingale.Centering
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) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)

Tactic:
(abs_sub _ _).trans (add_le_add (hω₁ i) (hω₂ i))

Premises used: abs_sub, add_le_add, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Centering
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) ω - f i ω - (predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω)| ≤ (↑(R + R) : ℝ)

Tactic:
exact (abs_sub _ _).trans (add_le_add (hω₁ i) (hω₂ i))

Premises used: abs_sub, add_le_add, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : upcrossings a b f ω ≠ ∞
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
rw [← lt_top_iff_ne_top, upcrossings_lt_top_iff] at hω

Premises used: lt_top_iff_ne_top, MeasureTheory.upcrossings_lt_top_iff
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
obtain :
  ∀ (k : ℕ) (hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k), ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k

Tactic:
obtain ⟨k, hk⟩ := hω