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
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)
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)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have compl : Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
  (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
Tactic: rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
-- 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 Ω
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)
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)
compl :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have compl₁ : Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
  (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle)
Tactic: rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
-- 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 Ω
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)
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)
compl :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
compl₁ :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle)
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have compl₂ : HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle) =
  ∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle
Tactic: rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
-- 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 Ω
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)
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)
compl :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
compl₁ :
  Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ.trim hle)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle)
compl₂ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g x ∂μ.trim hle) =
    ∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ.trim hle
⊢ Eq (α := ℝ) (∫ (x : Ω) in tᶜ, g x ∂μ)
    (∫ (x : Ω) in tᶜ, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have compl₃ : HSub.hSub (α := ℝ) (∫ (x : Ω), g x ∂μ.trim hle) (∫ (x : Ω) in t, g 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: rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
-- 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 Ω
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set Ω
hf : Pairwise (Function.onFun Disjoint f)
hfmeas : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : Ω) in f i, g x ∂μ)
        (∫ (x : Ω) in f i, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : Ω) in ⋃ (i : ℕ), f i, g x ∂μ)
    (∫ (x : Ω) in ⋃ (i : ℕ), f i, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have iUnion : Eq (α := ℝ) (∑' (n : ℕ), ∫ (x : Ω) in f n, g x ∂μ)
  (∑' (n : ℕ), ∫ (x : Ω) in f n, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
Tactic: rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
      integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
-- 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∞)
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
⊢ Eq (α := ℝ) (∫ (x : Ω) in s, g x ∂μ)
    (∫ (x : Ω) in s, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)
have empty : 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: induction s, hs
    using MeasurableSpace.induction_on_inter (MeasurableSpace.measurableSpace_iSup_eq ℱ) hpi with
  | empty =>
    simp only [Measure.restrict_empty, integral_zero_measure]
  | basic s hs =>
    rcases hs with ⟨n, hn⟩
    exact this n _ hn
  | compl t htmeas ht =>
    have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
    have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
      (hlimint.trim hle stronglyMeasurable_limitProcess)
    rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
  | iUnion f hf hfmeas heq =>
    rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
      integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
    exact tsum_congr fun n => heq _ (measure_lt_top _ _)
Cleared hypotheses: hs, h
-- 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∞)
hpi : IsPiSystem.{u_1} (α := Ω) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s}
empty :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ) (∫ (x : Ω) in ∅, g x ∂μ)
      (∫ (x : Ω) in ∅, 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 ∂μ)
have basic : ∀ (s : Set Ω) (hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | ∃ (n : ℕ), MeasurableSet s} 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: induction s, hs
    using MeasurableSpace.induction_on_inter (MeasurableSpace.measurableSpace_iSup_eq ℱ) hpi with
  | empty =>
    simp only [Measure.restrict_empty, integral_zero_measure]
  | basic s hs =>
    rcases hs with ⟨n, hn⟩
    exact this n _ hn
  | compl t htmeas ht =>
    have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)
    have hheq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas
      (hlimint.trim hle stronglyMeasurable_limitProcess)
    rw [setIntegral_trim hle hgmeas htmeas.compl,
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas.compl, hgeq, hheq, ←
      setIntegral_trim hle hgmeas htmeas, ←
      setIntegral_trim hle stronglyMeasurable_limitProcess htmeas, ← integral_trim hle hgmeas, ←
      integral_trim hle stronglyMeasurable_limitProcess, ← setIntegral_univ,
      this 0 _ MeasurableSet.univ, setIntegral_univ, ht (measure_lt_top _ _)]
  | iUnion f hf hfmeas heq =>
    rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
      integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]
    exact tsum_congr fun n => heq _ (measure_lt_top _ _)
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
have ht : ∀ᵐ (x : Ω) ∂μ,
  Tendsto (fun (n : ℕ) ↦ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
    (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
Tactic: have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x)
      atTop (𝓝 ((μ[g | ⨆ n, ℱ n]) x)) :=
    integrable_condExp.tendsto_ae_condExp stronglyMeasurable_condExp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
have heq : ∀ (n : ℕ),
  ∀ᵐ (x : Ω) ∂μ,
    μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
Tactic: have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x = (μ[g | ℱ n]) x := fun n =>
    condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
have heq₁ : ∀ᵐ (a : Ω) ∂μ,
  ∀ (i : ℕ),
    μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) i] a =
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
Tactic: rw [← ae_all_iff] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
heq :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) i] a =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i] a
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
have h : ∀ (x : Ω)
  (hxeq :
    ∀ (i : ℕ),
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) i] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i] x)
  (hxt :
    Tendsto (fun (n : ℕ) ↦ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))),
  Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
    (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))
Tactic: filter_upwards [heq, ht] with x hxeq hxt
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ)
    atTop (𝓝 0)
have ht : Tendsto (β := ℝ≥0∞)
  (fun (n : ℕ) ↦
    eLpNorm
      (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
        μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
      1 μ)
  atTop (𝓝 0)
Tactic: have ht : Tendsto (fun n => eLpNorm (μ[μ[g | ⨆ n, ℱ n] | ℱ n] - μ[g | ⨆ n, ℱ n]) 1 μ)
      atTop (𝓝 0) :=
    integrable_condExp.tendsto_eLpNorm_condExp stronglyMeasurable_condExp
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
ht :
  Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm
        (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
          μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
        1 μ)
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ)
    atTop (𝓝 0)
have heq : ∀ (n : ℕ),
  ∀ᵐ (x : Ω) ∂μ,
    μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
Tactic: have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g | ⨆ n, ℱ n] | ℱ n]) x = (μ[g | ℱ n]) x := fun n =>
    condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)