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 : Martingale f ℱ μ
n : ℕ
rw :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ _x ∈ Finset.range n, 0)
⊢ predictablePart f ℱ μ n =ᶠ[ae μ] 0

Tactic:
rw [predictablePart, ← Finset.sum_const_zero (s := Finset.range n)]

Premises used: Finset.sum_const_zero, 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
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)

Tactic:
eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- 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 : Martingale f ℱ μ
n : ℕ
refine : ∀ (i : ℕ) (hi : i ∈ Finset.range n), μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (∑ i ∈ Finset.range n, μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])
    (∑ _x ∈ Finset.range n, 0)

Tactic:
refine eventuallyEq_sum fun i hi => ?_

Premises used: eventuallyEq_sum
-- 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 : 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]

Tactic:
simp [condExp_sub (hf.integrable (i + 1)) (hf.integrable i) (ℱ i)]

Premises used: MeasureTheory.Martingale.integrable, MeasureTheory.Filtration.seq, HAdd.hAdd, OfNat.ofNat, MeasureTheory.condExp_sub
-- 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 : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) | (↑ℱ : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i - f i

Tactic:
(hf.condExp_ae_eq (Nat.le_succ i)).sub (hf.condExp_ae_eq le_rfl)

Premises used: le_rfl, Nat.le_succ, MeasureTheory.Martingale.condExp_ae_eq, Filter.EventuallyEq.sub
-- 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 : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ f i - f i =ᶠ[ae μ] 0

Tactic:
simp
-- 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 : 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 - f i =ᶠ[ae μ] 0
⊢ μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) 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

Premises used: le_rfl, MeasureTheory.Filtration.seq, Nat.le_succ, HAdd.hAdd, MeasureTheory.Martingale.condExp_ae_eq, OfNat.ofNat, Filter.EventuallyEq.sub
-- 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
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
⊢ ∀ᵐ (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
-- 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
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 :
  ∀ (ω : Ω) (h : ∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i] ω),
    Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
⊢ ∀ᵐ (ω : Ω) ∂μ, Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω

Tactic:
filter_upwards [this] with ω h
-- 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
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] ω
⊢ ∀ (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

Premises used: Nat.succ_eq_add_one, ge_iff_le, Pi.zero_apply
-- 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
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 ω

Tactic:
monotone_nat_of_le_succ fun n ↦ (?_ : _ ≥ _)

Premises used: monotone_nat_of_le_succ
-- 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
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
h₁ : ∀ (n : ℕ), predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω
⊢ Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω

Tactic:
refine monotone_nat_of_le_succ fun n ↦ (?_ : _ ≥ _)

Premises used: monotone_nat_of_le_succ
-- 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
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 ω
h₄ h₅ : predictablePart f ℱ μ n ω ≤ predictablePart f ℱ μ n ω
⊢ predictablePart f ℱ μ (n + 1) ω ≥ predictablePart f ℱ μ n ω

Tactic:
grw [predictablePart_add_one, Pi.add_apply, h n, add_zero]

Premises used: Pi.add_apply, add_zero, MeasureTheory.predictablePart_add_one
-- 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
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
h :
  ∀ (ω : Ω) (hω : Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω) (n : ℕ),
    0 ≤ predictablePart f ℱ μ n ω
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω

Tactic:
filter_upwards [hf.monotone_predictablePart] with ω hω n

Premises used: MeasureTheory.Submartingale.monotone_predictablePart
-- 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
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
ω : Ω
hω : Monotone.{0, u_2} (β := E) fun (x : ℕ) ↦ predictablePart f ℱ μ x ω
n : ℕ
⊢ 0 ≤ predictablePart f ℱ μ n ω

Tactic:
simpa [predictablePart_zero] using hω (Nat.zero_le n)

Premises used: Nat.zero_le, MeasureTheory.predictablePart_zero
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
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))
⊢ predictablePart f ℱ μ n =ᶠ[ae μ] f n - f 0

Tactic:
simp only [predictablePart, ← Finset.sum_range_sub]

Premises used: MeasureTheory.predictablePart, Finset.sum_range_sub
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ 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:
eventuallyEq_sum fun i hi => (condExp_of_stronglyMeasurable (ℱ.le i)
    ((hf.measurable_add_one i).sub (hf.stronglyAdapted i))
    ((hfint (i + 1)).sub (hfint i))).eventuallyEq

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.condExp_of_stronglyMeasurable, eventuallyEq_sum, MeasureTheory.Integrable.sub, Eq.eventuallyEq, HAdd.hAdd, MeasureTheory.Filtration.le, MeasureTheory.IsStronglyPredictable.measurable_add_one, OfNat.ofNat, MeasureTheory.IsStronglyPredictable.stronglyAdapted
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
⊢ 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:
exact eventuallyEq_sum fun i hi => (condExp_of_stronglyMeasurable (ℱ.le i)
    ((hf.measurable_add_one i).sub (hf.stronglyAdapted i))
    ((hfint (i + 1)).sub (hfint i))).eventuallyEq

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.condExp_of_stronglyMeasurable, eventuallyEq_sum, MeasureTheory.Integrable.sub, Eq.eventuallyEq, HAdd.hAdd, MeasureTheory.Filtration.le, MeasureTheory.IsStronglyPredictable.measurable_add_one, OfNat.ofNat, MeasureTheory.IsStronglyPredictable.stronglyAdapted
-- 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
⊢ StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ predictablePart f ℱ μ (n + 1)

Tactic:
fun _ => Finset.stronglyMeasurable_sum _ fun _ hin =>
    stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_succ_iff.mp hin))

Premises used: Finset.mem_range_succ_iff, Finset.stronglyMeasurable_sum, Finset.range, MeasureTheory.StronglyAdapted, HAdd.hAdd, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.predictablePart, Iff.mp, MeasureTheory.Filtration.mono, OfNat.ofNat
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ StronglyMeasurable (predictablePart f ℱ μ 0)

Tactic:
measurability
-- 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
⊢ StronglyAdapted (β := fun (n : ℕ) ↦ E) ℱ fun (n : ℕ) ↦ predictablePart f ℱ μ n

Tactic:
fun _ => Finset.stronglyMeasurable_sum _ fun _ hin =>
    stronglyMeasurable_condExp.mono (ℱ.mono (Finset.mem_range_le hin))

Premises used: Finset.stronglyMeasurable_sum, Finset.range, MeasureTheory.StronglyAdapted, Finset.mem_range_le, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.predictablePart, MeasureTheory.Filtration.mono
-- 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
⊢ martingalePart f ℱ μ 0 = f 0

Tactic:
simp [martingalePart]

Premises used: MeasureTheory.martingalePart
-- 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
c : ℝ
n : ℕ
h :
  ∀ (ω : Ω) (hω : predictablePart (c • f) ℱ μ n ω = (c • predictablePart f ℱ μ n) ω),
    martingalePart (c • f) ℱ μ n ω = (c • martingalePart f ℱ μ n) ω
⊢ martingalePart (c • f) ℱ μ n =ᶠ[ae μ] c • martingalePart f ℱ μ n

Tactic:
filter_upwards [predictablePart_smul (f := f) c n] with ω hω

Premises used: MeasureTheory.predictablePart_smul
-- 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
c : ℝ
n : ℕ
ω : Ω
hω : predictablePart (c • f) ℱ μ n ω = (c • predictablePart f ℱ μ n) ω
⊢ martingalePart (c • f) ℱ μ n ω = (c • martingalePart f ℱ μ n) ω

Tactic:
simpa [martingalePart, smul_sub]

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

Tactic:
filter_upwards [predictablePart_add (ℱ := ℱ) hfint hgint n] with ω hω

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

Tactic:
simp_all [martingalePart]

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

Tactic:
abel
-- 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 : Martingale f ℱ μ
n : ℕ
h : ∀ (ω : Ω) (hω : predictablePart f ℱ μ n ω = 0 ω), martingalePart f ℱ μ n ω = f n ω
⊢ martingalePart f ℱ μ n =ᶠ[ae μ] f n

Tactic:
filter_upwards [hf.predictablePart_eq_zero n] with ω hω

Premises used: MeasureTheory.Martingale.predictablePart_eq_zero
-- 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 : Martingale f ℱ μ
n : ℕ
ω : Ω
hω : predictablePart f ℱ μ n ω = 0 ω
⊢ martingalePart f ℱ μ n ω = f n ω

Tactic:
simp [martingalePart, hω]

Premises used: MeasureTheory.martingalePart
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
h : ∀ (ω : Ω) (hω : predictablePart f ℱ μ n ω = (f n - f 0) ω), martingalePart f ℱ μ n ω = f 0 ω
⊢ martingalePart f ℱ μ n =ᶠ[ae μ] f 0

Tactic:
filter_upwards [hf.predictablePart_eq (μ := μ) hfint n] with ω hω

Premises used: MeasureTheory.IsStronglyPredictable.predictablePart_eq
-- 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 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
ω : Ω
hω : predictablePart f ℱ μ n ω = (f n - f 0) ω
⊢ martingalePart f ℱ μ n ω = f 0 ω

Tactic:
simp [martingalePart, hω, sub_eq_add_neg]

Premises used: MeasureTheory.martingalePart, sub_eq_add_neg
-- Module: Mathlib.Probability.Martingale.Centering
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
ℱ : Filtration ℕ m0
μ : Measure Ω
f : ℕ → Ω → E
⊢ martingalePart f ℱ μ + predictablePart f ℱ μ = f

Tactic:
sub_add_cancel _ _

Premises used: MeasureTheory.martingalePart, sub_add_cancel
-- 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
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])
⊢ martingalePart f ℱ μ = fun (n : ℕ) ↦
    f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | (↑ℱ : ℕ → MeasurableSpace Ω) i])

Tactic:
unfold martingalePart predictablePart

Premises used: MeasureTheory.martingalePart, 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
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
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])
⊢ 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:
ext1 n
-- 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
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])
h₂ 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])
⊢ 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:
rw [Finset.eq_sum_range_sub f n, ← add_sub, ← Finset.sum_sub_distrib]

Premises used: add_sub, Finset.sum_sub_distrib, Finset.eq_sum_range_sub
-- 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
hf : StronglyAdapted (β := fun (i : ℕ) ↦ E) ℱ f
⊢ StronglyAdapted (β := fun (a : ℕ) ↦ E) ℱ (martingalePart f ℱ μ)

Tactic:
hf.sub stronglyAdapted_predictablePart'

Premises used: MeasureTheory.martingalePart, 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
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst_2 : CompleteSpace E
hf_int : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
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)
    μ
⊢ Integrable (martingalePart f ℱ μ n) μ

Tactic:
rw [martingalePart_eq_sum]

Premises used: MeasureTheory.martingalePart_eq_sum