awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
x : Ω
⊢ f i x ≤ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x
have base : f i x ≤ f i x
Tactic: rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have h : ∀ (ω : Ω) (hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) 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 i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: filter_upwards [hk, condExp_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
ω : Ω
hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) 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 i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: grw [hω1, hω2, hω3]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
ω : Ω
hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) 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 | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ f i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h₁ : μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤
  μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: grw [hω1, hω2, hω3]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j k : ℕ
hik : i ≤ k
hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
ω : Ω
hω1 : f i ω ≤ μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) 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 | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
h₁ :
  μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤
    μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ f i ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h₂ : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω ≤ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: grw [hω1, hω2, hω3]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have base : f i ≤ᶠ[ae μ] μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) 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_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3
    grw [hω1, hω2, hω3]
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i j : ℕ
hij : i ≤ j
base : f i ≤ᶠ[ae μ] μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ f i ≤ᶠ[ae μ] μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have succ : ∀ (k : ℕ) (hik : i ≤ k) (hk : f i ≤ᶠ[ae μ] μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i]),
  f i ≤ᶠ[ae μ] μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) 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_mono (hint k) integrable_condExp (hf k),
      𝒢.condExp_condExp (f (k + 1)) hik] with ω hω1 hω2 hω3
    grw [hω1, hω2, hω3]
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
⊢ Supermartingale f 𝒢 μ
have rw : Supermartingale (- -f) 𝒢 μ
Tactic: rw [← neg_neg f]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
⊢ Supermartingale (- -f) 𝒢 μ
have refine : ∀ (i : ℕ), (-f) i ≤ᶠ[ae μ] -μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine (submartingale_nat hadp.neg (fun i => (hint i).neg) fun i =>
    EventuallyLE.trans ?_ (condExp_neg ..).symm.le).neg
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
i : ℕ
⊢ (-f) i ≤ᶠ[ae μ] -μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x ≤ f i x) x}
          x →
        Membership.mem (γ := Set Ω)
          {x : Ω | (fun (x : Ω) ↦ (-f) i x ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) x) x} x}
    a
Tactic: filter_upwards [hf i] with x hx using neg_le_neg hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : ℕ), μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ≤ᶠ[ae μ] f i
i : ℕ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x ≤ f i x) x}
            x →
          Membership.mem (γ := Set Ω)
            {x : Ω | (fun (x : Ω) ↦ (-f) i x ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) x) x} x}
      a
⊢ (-f) i ≤ᶠ[ae μ] -μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have h₁ : ∀ (a : Ω),
  μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] a ≤ f i a →
    (-f) i a ≤ (-μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) a
Tactic: filter_upwards [hf i] with x hx using neg_le_neg hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
⊢ Submartingale f 𝒢 μ
have refine : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine submartingale_nat hadp hint fun i => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
i : ℕ
⊢ f i ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have rw : 0 ≤ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: rw [← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _), ← eventually_sub_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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]
⊢ Supermartingale f 𝒢 μ
have rw : Supermartingale (- -f) 𝒢 μ
Tactic: rw [← neg_neg f]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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]
⊢ Supermartingale (- -f) 𝒢 μ
have refine : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 : ℕ
⊢ f 0 ≤ᶠ[ae μ] f n
have zero : f 0 ≤ᶠ[ae μ] f 0
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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f 0 ≤ᶠ[ae μ] f n
have succ : ∀ (k : ℕ) (ih : f 0 ≤ᶠ[ae μ] f k), f 0 ≤ᶠ[ae μ] f (k + 1)
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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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 : ℕ
⊢ f n ≤ᶠ[ae μ] f 0
have zero : f 0 ≤ᶠ[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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (goal)
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
⊢ f n ≤ᶠ[ae μ] f 0
have succ : ∀ (k : ℕ) (ih : f k ≤ᶠ[ae μ] f 0), f (k + 1) ≤ᶠ[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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 𝒢 μ
have refine : ∀ (i j : ℕ) (hij : i ≤ j), μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
Tactic: refine ⟨hadp, fun i j hij ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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
have base : ∀ (x : Ω), μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x = f i x
Tactic: refine ae_of_all _ fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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 : Ω
⊢ μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] x = f i x
have base : f i x = f i x
Tactic: rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
have 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 ω
Tactic: filter_upwards [hk, condExp_congr_ae (hf k), 𝒢.condExp_condExp (f (k + 1)) hik]
      with ω hω1 hω2 hω3
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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] ω
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω
have h : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: rw [← hω1, hω2, hω3]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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] ω
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω
have h₁ : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
  μ[μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) k] | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: rw [← hω1, hω2, hω3]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (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 : 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] ω
⊢ μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = f i ω
have h₂ : μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω = μ[f (k + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: rw [← hω1, hω2, hω3]