awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
refine : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.StronglyAdapted.neg, MeasureTheory.submartingale_of_condExp_sub_nonneg_nat, MeasureTheory.Submartingale.neg
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedModule ℝ E
inst_7 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
simpa only [Pi.zero_apply, Pi.neg_apply, neg_sub_neg]

Premises used: Pi.zero_apply, neg_sub_neg, Pi.neg_apply
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f 0 ≤ᶠ[ae μ] f k
⊢ f 0 ≤ᶠ[ae μ] f (k + 1)

Tactic:
ih.trans ((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq <| Germ.coe_eq.mp <|
    congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _)

Premises used: Filter.Germ.ofFun, Filter.EventuallyLE.trans_eq, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_of_stronglyMeasurable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, And.left, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyLE.trans
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f 0 ≤ᶠ[ae μ] f k
⊢ f 0 ≤ᶠ[ae μ] f (k + 1)

Tactic:
exact ih.trans ((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq <| Germ.coe_eq.mp <|
    congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _)

Premises used: Filter.Germ.ofFun, Filter.EventuallyLE.trans_eq, MeasureTheory.Submartingale.integrable, MeasureTheory.condExp_of_stronglyMeasurable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, And.left, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyLE.trans
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
n : ℕ
zero : f 0 ≤ᶠ[ae μ] f 0
succ : ∀ (k : ℕ) (ih : f 0 ≤ᶠ[ae μ] f k), f 0 ≤ᶠ[ae μ] f (k + 1)
⊢ f 0 ≤ᶠ[ae μ] f n

Tactic:
induction n with
  | zero => rfl
  | succ k ih =>
    exact ih.trans ((hfmgle.2.1 k (k + 1) k.le_succ).trans_eq <| Germ.coe_eq.mp <|
    congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _)
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f k ≤ᶠ[ae μ] f 0
⊢ f (k + 1) ≤ᶠ[ae μ] f 0

Tactic:
((Germ.coe_eq.mp <| congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _)
      (hfadp _) <| hfmgle.integrable _).symm.trans_le (hfmgle.2.1 k (k + 1) k.le_succ)).trans ih

Premises used: Filter.Germ.ofFun, MeasureTheory.condExp_of_stronglyMeasurable, Filter.EventuallyEq.trans_le, MeasureTheory.Supermartingale.integrable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, And.left, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f k ≤ᶠ[ae μ] f 0
⊢ f (k + 1) ≤ᶠ[ae μ] f 0

Tactic:
exact ((Germ.coe_eq.mp <| congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _)
      (hfadp _) <| hfmgle.integrable _).symm.trans_le (hfmgle.2.1 k (k + 1) k.le_succ)).trans ih

Premises used: Filter.Germ.ofFun, MeasureTheory.condExp_of_stronglyMeasurable, Filter.EventuallyEq.trans_le, MeasureTheory.Supermartingale.integrable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, And.left, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : Preorder E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
n : ℕ
zero : f 0 ≤ᶠ[ae μ] f 0
succ : ∀ (k : ℕ) (ih : f k ≤ᶠ[ae μ] f 0), f (k + 1) ≤ᶠ[ae μ] f 0
⊢ f n ≤ᶠ[ae μ] f 0

Tactic:
induction n with
  | zero => rfl
  | succ k ih =>
    exact ((Germ.coe_eq.mp <| congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _)
      (hfadp _) <| hfmgle.integrable _).symm.trans_le (hfmgle.2.1 k (k + 1) k.le_succ)).trans ih
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Martingale f 𝒢 μ

Tactic:
⟨hadp, fun i j hij ↦ ?_⟩

Premises used: MeasureTheory.Martingale, And.intro
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
refine : ∀ (i j : ℕ) (hij : i ≤ j), μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
⊢ Martingale f 𝒢 μ

Tactic:
refine ⟨hadp, fun i j hij ↦ ?_⟩
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
⊢ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i

Tactic:
ae_of_all _ fun _ ↦ ?_

Premises used: Filter.EventuallyEq, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
base : ∀ (x : Ω), μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x = f i x
⊢ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i

Tactic:
refine ae_of_all _ fun _ ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
x : Ω
base base₁ : f i x = f i x
⊢ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x = f i x

Tactic:
rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
h :
  ∀ (ω : Ω) (hω1 : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω)
    (hω2 :
      μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
        μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω)
    (hω3 :
      μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
        μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω),
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i

Tactic:
filter_upwards [hk, condExp_congr_ae (hf k), 𝒢.condExp_condExp (f (k + 1)) hik]
      with ω hω1 hω2 hω3

Premises used: MeasureTheory.Filtration.condExp_condExp, MeasureTheory.condExp_congr_ae, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
ω : Ω
hω1 : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω
hω2 :
  μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω3 :
  μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₁ :
  μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₂ h₃ : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω

Tactic:
rw [← hω1, hω2, hω3]
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
hij : i ≤ j
base : μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
succ :
  ∀ (k : ℕ) (hik : i ≤ k) (hk : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i),
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
⊢ μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i

Tactic:
induction j, hij using Nat.le_induction with
  | base =>
    refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
  | succ k hik hk =>
    filter_upwards [hk, condExp_congr_ae (hf k), 𝒢.condExp_condExp (f (k + 1)) hik]
      with ω hω1 hω2 hω3
    rw [← hω1, hω2, hω3]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.ae_of_all, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (i : ℕ) (s : Set Ω),
    MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
⊢ Martingale f 𝒢 μ

Tactic:
martingale_nat hadp hint fun n ↦ ae_eq_of_ae_eq_trim <|
    ((hint n).trim (𝒢.le n) (hadp n)).ae_eq_of_forall_setIntegral_eq _ _
    (integrable_condExp.trim (𝒢.le n) stronglyMeasurable_condExp) fun s ms hs ↦ ?_

Premises used: MeasureTheory.Filtration.seq, MeasureTheory.integrable_condExp, MeasureTheory.condExp, MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq, MeasureTheory.martingale_nat, HAdd.hAdd, MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Filtration.le, OfNat.ofNat, MeasureTheory.Integrable.trim
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (i : ℕ) (s : Set Ω),
    MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
refine :
  ∀ (n : ℕ) (s : Set Ω) (ms : MeasurableSet s)
    (hs : LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
      (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
⊢ Martingale f 𝒢 μ

Tactic:
refine martingale_nat hadp hint fun n ↦ ae_eq_of_ae_eq_trim <|
    ((hint n).trim (𝒢.le n) (hadp n)).ae_eq_of_forall_setIntegral_eq _ _
    (integrable_condExp.trim (𝒢.le n) stronglyMeasurable_condExp) fun s ms hs ↦ ?_

Premises used: MeasureTheory.Filtration.seq, MeasureTheory.integrable_condExp, MeasureTheory.condExp, MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq, MeasureTheory.martingale_nat, HAdd.hAdd, MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Filtration.le, OfNat.ofNat, MeasureTheory.Integrable.trim
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (i : ℕ) (s : Set Ω),
    MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f i ω ∂μ) (∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
n : ℕ
s : Set Ω
ms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ) (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ)
rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ) (∫ (x : Ω) in s, f (n + 1) x ∂μ)
rw₃ rw₄ : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f (n + 1) ω ∂μ) (∫ (x : Ω) in s, f (n + 1) x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)

Tactic:
rw [← setIntegral_trim (𝒢.le n) (hadp n) ms,
    ← setIntegral_trim (𝒢.le n) stronglyMeasurable_condExp ms,
    setIntegral_condExp (𝒢.le n) (hint (n + 1)) ms, hf n s ms]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.setIntegral_trim, HAdd.hAdd, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Filtration.le, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
⊢ Martingale f 𝒢 μ

Tactic:
martingale_nat hadp hint fun i ↦ ?_

Premises used: MeasureTheory.martingale_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
refine : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Martingale f 𝒢 μ

Tactic:
refine martingale_nat hadp hint fun i ↦ ?_

Premises used: MeasureTheory.martingale_nat
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
i : ℕ
rw : μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
⊢ f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]

Tactic:
rw [← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _),
    eventuallyEq_comm, eventuallyEq_iff_sub]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, Filter.eventuallyEq_iff_sub, MeasureTheory.Filtration.le, Filter.eventuallyEq_comm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
i : ℕ
⊢ μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0

Tactic:
EventuallyEq.trans (condExp_sub (hint _) (hint _) _).symm (hf i)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted (β := fun (i : ℕ) ↦ E) 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
i : ℕ
⊢ μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0

Tactic:
exact EventuallyEq.trans (condExp_sub (hint _) (hint _) _).symm (hf i)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
⊢ f 0 =ᶠ[ae μ] f 0

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f k =ᶠ[ae μ] f 0
⊢ f (k + 1) =ᶠ[ae μ] f 0

Tactic:
((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
      (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih

Premises used: Filter.Germ.ofFun, Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_of_stronglyMeasurable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
k : ℕ
ih : f k =ᶠ[ae μ] f 0
⊢ f (k + 1) =ᶠ[ae μ] f 0

Tactic:
exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
      (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih

Premises used: Filter.Germ.ofFun, Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_of_stronglyMeasurable, Nat.le_succ, Filter.Germ.coe_eq, congr_arg, And.right, HAdd.hAdd, Iff.mp, MeasureTheory.Filtration.le, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Martingale.Basic
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ f (n + 1)
n : ℕ
zero : f 0 =ᶠ[ae μ] f 0
succ : ∀ (k : ℕ) (ih : f k =ᶠ[ae μ] f 0), f (k + 1) =ᶠ[ae μ] f 0
⊢ f n =ᶠ[ae μ] f 0

Tactic:
induction n with
  | zero => rfl
  | succ k ih =>
    exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
      (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih