awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
this :
  (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞ ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
have ht : ENNReal.ofReal (b - a) ≠ ∞
Tactic: left
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
have simp : ∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i : ℝ) (↑i_1 : ℝ) f x < ∞
Tactic: simp only [ae_all_iff, eventually_imp_distrib_left]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h : ∀ (ω : Ω) (h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞)
  (h₂ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n ω‖ₑ) atTop) ∞),
  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: filter_upwards [hf.upcrossings_ae_lt_top hbdd, ae_bdd_liminf_atTop_of_eLpNorm_bdd one_ne_zero
    (fun n => (hf.stronglyMeasurable n).measurable.mono (ℱ.le n) le_rfl) hbdd] with ω h₁ h₂
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)} : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [ae_iff, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have hs : MeasurableSet.{u_1} (α := Ω) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)}
Tactic: rw [ae_iff, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have rw : ∀ᵐ (ω : Ω) ∂μ,
  Tendsto (fun (n : ℕ) ↦ f n ω) atTop
    (𝓝
      (Classical.choose (p := fun (x : Ω → ℝ) ↦
        StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) this ω))
Tactic: rw [limitProcess, dif_pos this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₁ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
Tactic: have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
have h : ∀ (ω : Ω) (hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
Tactic: filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
ω : Ω
hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
have h : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (hω.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))))
Tactic: simp_rw [g', dif_pos hω]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
Tactic: have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have hg'm : AEStronglyMeasurable g' (μ.trim hle)
Tactic: have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
hg'm : AEStronglyMeasurable g' (μ.trim hle)
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have obtain : ∀ (g : Ω → ℝ) (hgm : StronglyMeasurable g) (hae : g' =ᶠ[ae (μ.trim hle)] g),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: obtain ⟨g, hgm, hae⟩ := hg'm
Cleared hypotheses: hg'm
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have h : ∀ (ω : Ω) (hω : g' ω = g ω) (hg'ω : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
  Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: filter_upwards [hae, hg'] with ω hω hg'ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
have hg : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₁ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ ℱ₂ ℱ₃ ℱ₄ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₅ : ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ ℱ₂ ℱ₃ ℱ₄ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₅ :
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₆ : let g' : Ω → ℝ := fun (ω : Ω) ↦
  if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
    h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
  else 0;
∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
  (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ ℱ₂ ℱ₃ ℱ₄ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₅ :
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₆ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₇ : let g' : Ω → ℝ := fun (ω : Ω) ↦
  if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
    h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
  else 0;
∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
  (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω)))
  (hg'm : AEStronglyMeasurable g' (μ.trim hle)),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ ℱ₂ ℱ₃ ℱ₄ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₅ :
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₆ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
ℱ₇ :
  let g' : Ω → ℝ := fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0;
  ∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
    (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω)))
    (hg'm : AEStronglyMeasurable g' (μ.trim hle)),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
have ℱ₈ : let g' : Ω → ℝ := fun (ω : Ω) ↦
  if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
    h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
  else 0;
∀ (hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0)
  (hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))) (g : Ω → ℝ)
  (hgm : StronglyMeasurable g) (hae : g' =ᶠ[ae (μ.trim hle)] g),
  ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
Tactic: classical
  suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
  set g' : Ω → ℝ := fun ω => if h : ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) then h.choose else 0
  have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
  have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
  have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
  obtain ⟨g, hgm, hae⟩ := hg'm
  have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
  exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
have obtain : ∀ (R : ℝ≥0) (hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)),
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
Tactic: obtain ⟨R, hR⟩ := hunif.2.2
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
have hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
Tactic: have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
    ((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable