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 : 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 j | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
have base : μ[f i | (↑𝒢 : ℕ → 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]
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 : 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
⊢ μ[f j | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i
have succ : ∀ (k : ℕ) (hik : i ≤ k) (hk : μ[f k | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] f i),
  μ[f (k + 1) | (↑𝒢 : ℕ → 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]
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 : 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 𝒢 μ
have refine : ∀ (n : ℕ) (s : Set Ω) (ms : MeasurableSet s)
  (hs : LT.lt (α := ℝ≥0∞) ((μ.trim sorry : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim sorry)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim sorry)
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 ↦ ?_
-- 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 : ℕ) (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∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ)
  (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim sorry)
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]
-- 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 : ℕ) (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 ⋯)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ) (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ)
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]
-- 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 : ℕ) (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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ) (∫ (x : Ω) in s, f (n + 1) x ∂μ)
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]
-- 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 : ℕ) (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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, f n x ∂μ.trim ⋯)
    (∫ (x : Ω) in s, μ[f (n + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) n] x ∂μ.trim ⋯)
have rw₃ : Eq.{u_2 + 1} (α := E) (∫ (ω : Ω) in s, f (n + 1) ω ∂μ) (∫ (x : Ω) in s, f (n + 1) x ∂μ)
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]
-- 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 + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
⊢ Martingale f 𝒢 μ
have refine : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine martingale_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 : 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 =ᶠ[ae μ] μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have rw : μ[f (i + 1) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] - μ[f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] =ᶠ[ae μ] 0
Tactic: rw [← condExp_of_stronglyMeasurable (𝒢.le _) (hadp _) (hint _),
    eventuallyEq_comm, eventuallyEq_iff_sub]
-- 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 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale 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 (hfmgle.2 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 : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale 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 (hfmgle.2 k (k + 1) k.le_succ)).trans ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
have hξbdd : ∀ (i : ℕ), ∃ (C : ℝ), ∀ (ω : Ω), ‖ξ i ω‖ ≤ C
Tactic: have hξbdd : ∀ i, ∃ C, ∀ ω, ‖ξ i ω‖ ≤ C := fun i =>
    ⟨R, fun ω => (abs_of_nonneg (hnonneg i ω)).trans_le (hbdd 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
hξbdd : ∀ (i : ℕ), ∃ (C : ℝ), ∀ (ω : Ω), ‖ξ i ω‖ ≤ C
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
have choose : ∀ (C : (i : ℕ) → ℝ) (hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i),
  Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
Tactic: choose C hC using hξbdd
Cleared hypotheses: hξbdd
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
have hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
Tactic: have hint : ∀ m, Integrable (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ := fun m =>
      integrable_finsetSum' _ fun i _ => Integrable.bdd_smul
        ((hf.integrable _).sub (hf.integrable _)) (C i)
        hξ.stronglyMeasurable.aestronglyMeasurable (ae_of_all _ (hC 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m : ℕ
⊢ StronglyMeasurable.{u_1, u_2} (α := Ω) (β := (fun (n : ℕ) ↦ E) m)
    ((fun (n : ℕ) ↦ (∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k) : Ω → E)) m)
have refine : ∀ (i : ℕ) (hi : i ∈ Finset.range m), StronglyMeasurable (ξ i • (f (i + 1) - f i))
Tactic: refine Finset.stronglyMeasurable_sum _ fun i hi => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
m i : ℕ
hi : i ∈ Finset.range m
⊢ StronglyMeasurable (ξ i • (f (i + 1) - f i))
have hi₁ : i < m
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Probability.Martingale.Basic (hypothesis)
Goal:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
have hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
Tactic: have hadp : StronglyAdapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k) := by
    intro m
    refine Finset.stronglyMeasurable_sum _ fun i hi => ?_
    rw [Finset.mem_range] at hi
    exact (hξ.stronglyMeasurable_le hi.le).smul
      ((hf.stronglyAdapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub
        (hf.stronglyAdapted.stronglyMeasurable_le hi.le))
-- 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
⊢ Submartingale.{u_1, u_2, 0} (E := E) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)) 𝒢 μ
have refine : ∀ (i : ℕ),
  0 ≤ᶠ[ae μ]
    μ[HSub.hSub (α := Ω → E) (∑ k ∈ Finset.range (i + 1), ξ k • (f (k + 1) - f k))
        (∑ k ∈ Finset.range i, ξ k • (f (k + 1) - f k)) |
      (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: refine submartingale_of_condExp_sub_nonneg_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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
⊢ 0 ≤ᶠ[ae μ]
    μ[HSub.hSub (α := Ω → E) (∑ k ∈ Finset.range (i + 1), ξ k • (f (k + 1) - f k))
        (∑ k ∈ Finset.range i, ξ k • (f (k + 1) - f k)) |
      (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have simp : 0 ≤ᶠ[ae μ] μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
Tactic: simp only [← Finset.sum_Ico_eq_sub _ (Nat.le_succ _), Nat.succ_eq_add_one, Nat.Ico_succ_singleton,
    Finset.sum_singleton]
-- 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i]
have h : ∀ (ω : Ω) (hω1 : 0 ω ≤ μ[f i.succ - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω)
  (hω2 :
    μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
      (ξ i • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) ω),
  0 ω ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: filter_upwards [hf.condExp_sub_nonneg i.le_succ,
    condExp_smul_of_aestronglyMeasurable_left (hξ i).aestronglyMeasurable
      (((hf.integrable (i + 1)).sub (hf.integrable i)).bdd_smul
      (C i) hξ.stronglyMeasurable.aestronglyMeasurable (ae_of_all _ (hC i)))
      ((hf.integrable _).sub (hf.integrable _))] with ω hω1 hω2
-- 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ω ≤ μ[f i.succ - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    (ξ i • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i]) ω
⊢ 0 ω ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h : 0 ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
Tactic: simp only [Pi.zero_apply, Nat.succ_eq_add_one, Pi.smul_apply'] at hω1 hω2 ⊢
-- 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 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
inst_6 : IsOrderedAddMonoid E
inst_7 : IsFiniteMeasure μ
R : ℝ
f : ℕ → Ω → E
ξ : ℕ → Ω → ℝ
hf : Submartingale f 𝒢 μ
hξ : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) 𝒢 ξ
hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R
hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω
C : (i : ℕ) → ℝ
hC : ∀ (i : ℕ) (ω : Ω), ‖ξ i ω‖ ≤ C i
hint : ∀ (m : ℕ), Integrable.{u_2, u_1} (ε := E) (∑ k ∈ Finset.range m, ξ k • (f (k + 1) - f k)) μ
hadp : StronglyAdapted (β := fun (n : ℕ) ↦ E) 𝒢 fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, ξ k • (f (k + 1) - f k)
i : ℕ
ω : Ω
hω1 : 0 ≤ μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
hω2 :
  μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω =
    ξ i ω • μ[f (i + 1) - f i | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
⊢ 0 ≤ μ[ξ i • (f (i + 1) - f i) | (↑𝒢 : ℕ → MeasurableSpace Ω) i] ω
have h₁ : 0 ≤ ξ i ω
Tactic: grw [← smul_zero (0 : ℝ), hnonneg i ω, hω1, hω2]