awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ f n =ᶠ[ae μ] μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]
have rw : eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0
Tactic: rw [← sub_ae_eq_zero, ← eLpNorm_eq_zero_iff (((hf.stronglyMeasurable n).mono (ℱ.le _)).sub
    (stronglyMeasurable_condExp.mono (ℱ.le _))).aestronglyMeasurable one_ne_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0
have ht : Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ) atTop (𝓝 0)
Tactic: have ht : Tendsto (fun m => eLpNorm (μ[f m - g | ℱ n]) 1 μ) atTop (𝓝 0) :=
    haveI hint : ∀ m, Integrable (f m - g) μ := fun m => (hf.integrable m).sub hg
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hgtends (fun m => zero_le)
      fun m => eLpNorm_one_condExp_le_eLpNorm _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ) atTop (𝓝 0)
⊢ ∀ m ≥ n,
    eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ = eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
have refine : ∀ (m : ℕ) (hm : m ≥ n),
  μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]
Tactic: refine fun m hm => eLpNorm_congr_ae ((condExp_sub (hf.integrable m) hg _).trans ?_)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
⊢ μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]
have h : ∀ (x : Ω) (hx : μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] x = f n x),
  (μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) x =
    (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) x
Tactic: filter_upwards [hf.2 n m hm] with x hx
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ) atTop (𝓝 0)
⊢ eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0
have hev : ∀ m ≥ n,
  eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ = eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
Tactic: have hev : ∀ m ≥ n, eLpNorm (μ[f m - g | ℱ n]) 1 μ = eLpNorm (f n - μ[g | ℱ n]) 1 μ := by
    refine fun m hm => eLpNorm_congr_ae ((condExp_sub (hf.integrable m) hg _).trans ?_)
    filter_upwards [hf.2 n m hm] with x hx
    simp only [hx, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
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 (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
have hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
Tactic: have hunif : UniformIntegrable (fun n => μ[g | ℱ n]) 1 μ :=
    hg.uniformIntegrable_condExp_filtration
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
have obtain : ∀ (R : ℝ≥0)
  (hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)),
  ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
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
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
have hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
Tactic: have hlimint : Integrable (ℱ.limitProcess (fun n => μ[g | ℱ n]) μ) μ :=
    (memLp_limitProcess_of_eLpNorm_bdd hunif.1 hR).integrable le_rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this : g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
have h : ∀ (x : Ω) (heq : g x = limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x)
  (ht :
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (limitProcess (fun (i : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i]) ℱ μ x))),
  Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
Tactic: filter_upwards [this, (martingale_condExp g ℱ μ).submartingale.ae_tendsto_limitProcess hR] with
      x heq ht
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))
have suffices : g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ
Tactic: suffices g =ᵐ[μ] ℱ.limitProcess (fun n x => (μ[g | ℱ n]) x) μ by
    filter_upwards [this, (martingale_condExp g ℱ μ).submartingale.ae_tendsto_limitProcess hR] with
      x heq ht
    rwa [heq]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have rw : Eq (α := ℝ) (∫ (x : Ω) in s, μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
  (∫ (x : Ω) in s,
    μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
Tactic: rw [← setIntegral_condExp (ℱ.le n) hg hs, ← setIntegral_condExp (ℱ.le n) hlimint hs]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
    (∫ (x : Ω) in s,
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
have refine : ∀ᵐ (x : Ω) ∂μ,
  x ∈ s →
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
Tactic: refine setIntegral_congr_ae (ℱ.le _ _ hs) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ s →
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
have h : ∀ (x : Ω)
  (hx :
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[limitProcess (fun (i : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x),
  x ∈ s →
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
Tactic: filter_upwards [(martingale_condExp g ℱ μ).ae_eq_condExp_limitProcess hunif n] with x hx _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
x : Ω
hx :
  μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
    μ[limitProcess (fun (i : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
h : x ∈ s
⊢ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
    μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
have h : Eq (α := ℝ)
  (μ[limitProcess (fun (i : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x)
  (μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
⊢ g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ
have this : ∀ (n : ℕ) (s : Set Ω),
  MeasurableSet s →
    Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
      (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
Tactic: have : ∀ n s, MeasurableSet[ℱ n] s →
      ∫ x in s, g x ∂μ = ∫ x in s, ℱ.limitProcess (fun n x => (μ[g | ℱ n]) x) μ x ∂μ := by
    intro n s hs
    rw [← setIntegral_condExp (ℱ.le n) hg hs, ← setIntegral_condExp (ℱ.le n) hlimint hs]
    refine setIntegral_congr_ae (ℱ.le _ _ hs) ?_
    filter_upwards [(martingale_condExp g ℱ μ).ae_eq_condExp_limitProcess hunif n] with x hx _
    rw [hx]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
⊢ g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ
have refine : ∀ (s : Set Ω) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
      (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hle (fun s _ _ => hg.integrableOn)
    (fun s _ _ => hlimint.integrableOn) (fun s hs _ => ?_) hgmeas.aestronglyMeasurable
    stronglyMeasurable_limitProcess.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
have rw : IsPiSystem.{u_1} (α := Ω) (⋃ (i : ℕ), {x : Set Ω | MeasurableSet x})
Tactic: rw [Set.setOf_exists]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s : Set Ω
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
Tactic: have hpi : IsPiSystem {s | ∃ n, MeasurableSet[ℱ n] s} := by
    rw [Set.setOf_exists]
    exact isPiSystem_iUnion_of_monotone _ (fun n ↦ (ℱ n).isPiSystem_measurableSet) fun _ _ ↦ ℱ.mono
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s_1 : Set Ω
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
s : Set Ω
hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s} s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have basic : ∀ (n : ℕ) (hn : MeasurableSet s),
  Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
Tactic: rcases hs with ⟨n, hn⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s : Set Ω
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in t, g x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) tᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle)
Tactic: have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hunif : UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (ε := ℝ) ((fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) i) 1 μ ≤ (↑R : ℝ≥0∞)
hlimint : Integrable (ε := ℝ) (limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
        (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
s : Set Ω
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in t, g x ∂μ)
      (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) tᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
hgeq :
  ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have hheq : ∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle =
  HSub.hSub (α := ℝ) (∫ (x : Ω), limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
    (∫ (x : Ω) in t, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ.trim hle)
Tactic: have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
      (hlimint.trim hle stronglyMeasurable_limitProcess)