awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Convergence
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) ℱ μ
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))
⊢ ∀ᵐ (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

Premises used: MeasureTheory.martingale_condExp, MeasureTheory.Martingale.submartingale, MeasureTheory.Submartingale.ae_tendsto_limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
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 : Ω
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))
h h₁ h₂ h₃ :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
    (𝓝 (limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x))
⊢ Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))

Tactic:
rwa [heq]
-- Module: Mathlib.Probability.Martingale.Convergence
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]) ℱ μ) μ
suffices : g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g 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]
-- Module: Mathlib.Probability.Martingale.Convergence
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
rw :
  Eq (α := ℝ) (∫ (x : Ω) in s, μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
    (∫ (x : Ω) in s,
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
rw [← setIntegral_condExp (ℱ.le n) hg hs, ← setIntegral_condExp (ℱ.le n) hlimint hs]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Convergence
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 ∂μ)

Tactic:
setIntegral_congr_ae (ℱ.le _ _ hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Convergence
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
refine :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ s →
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)
    (∫ (x : Ω) in s,
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x ∂μ)

Tactic:
refine setIntegral_congr_ae (ℱ.le _ _ hs) ?_

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Convergence
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
⊢ x ∈ s →
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x

Tactic:
_
-- Module: Mathlib.Probability.Martingale.Convergence
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
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
⊢ ∀ᵐ (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 _

Premises used: MeasureTheory.martingale_condExp, MeasureTheory.Martingale.ae_eq_condExp_limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
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_1 : x ∈ s
h h₁ :
  Eq (α := ℝ)
    (μ[limitProcess (fun (i : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x)
    (μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x)
⊢ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
    μ[limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n] x

Tactic:
rw [hx]
-- Module: Mathlib.Probability.Martingale.Convergence
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 Ω),
    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]
-- Module: Mathlib.Probability.Martingale.Convergence
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) ℱ μ

Tactic:
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

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite', MeasureTheory.Filtration.stronglyMeasurable_limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
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 ∂μ)
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 ∂μ)
⊢ g =ᶠ[ae μ] limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 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

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite', MeasureTheory.Filtration.stronglyMeasurable_limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
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∞)
rw : IsPiSystem.{u_1} (α := Ω) (⋃ (i : ℕ), {x : Set Ω | MeasurableSet x})
⊢ IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}

Tactic:
rw [Set.setOf_exists]

Premises used: Set.setOf_exists
-- Module: Mathlib.Probability.Martingale.Convergence
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} (α := Ω) (⋃ (i : ℕ), {x : Set Ω | MeasurableSet x})

Tactic:
isPiSystem_iUnion_of_monotone _ (fun n ↦ (ℱ n).isPiSystem_measurableSet) fun _ _ ↦ ℱ.mono

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_iUnion_of_monotone, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Martingale.Convergence
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} (α := Ω) (⋃ (i : ℕ), {x : Set Ω | MeasurableSet x})

Tactic:
exact isPiSystem_iUnion_of_monotone _ (fun n ↦ (ℱ n).isPiSystem_measurableSet) fun _ _ ↦ ℱ.mono

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_iUnion_of_monotone, MeasureTheory.Filtration.mono
-- Module: Mathlib.Probability.Martingale.Convergence
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}

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
-- Module: Mathlib.Probability.Martingale.Convergence
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}
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : Ω) in ∅, g x ∂μ)
    (∫ (x : Ω) in ∅, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
simp only [Measure.restrict_empty, integral_zero_measure]

Premises used: MeasureTheory.Measure.restrict_empty, MeasureTheory.integral_zero_measure
-- Module: Mathlib.Probability.Martingale.Convergence
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∞)
basic :
  ∀ (n : ℕ) (hn : MeasurableSet s),
    Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
      (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
rcases hs with ⟨n, hn⟩
-- Module: Mathlib.Probability.Martingale.Convergence
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 Ω
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
n : ℕ
hn : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
this n _ hn
-- Module: Mathlib.Probability.Martingale.Convergence
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 Ω
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
n : ℕ
hn : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
exact this n _ hn