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 :
  ∀ (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∞)
⊢ ∫ (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)
-- 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}
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)
⊢ ∫ (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)
-- 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}
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∞)
iUnion :
  Eq (α := ℝ) (∑' (n : ℕ), ∫ (x : Ω) in f n, g x ∂μ)
    (∑' (n : ℕ), ∫ (x : Ω) in f n, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : Ω) in ⋃ (i : ℕ), f i, g x ∂μ)
    (∫ (x : Ω) in ⋃ (i : ℕ), f i, limitProcess (fun (n : ℕ) (x : Ω) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) ℱ μ x ∂μ)

Tactic:
rw [integral_iUnion (fun n => hle _ (hfmeas n)) hf hg.integrableOn,
      integral_iUnion (fun n => hle _ (hfmeas n)) hf hlimint.integrableOn]

Premises used: MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_iUnion
-- 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}
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 (α := ℝ) (∑' (n : ℕ), ∫ (x : Ω) in f n, g x ∂μ)
    (∑' (n : ℕ), ∫ (x : Ω) in f n, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)

Tactic:
tsum_congr fun n => heq _ (measure_lt_top _ _)

Premises used: tsum_congr, MeasureTheory.measure_lt_top
-- 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}
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 (α := ℝ) (∑' (n : ℕ), ∫ (x : Ω) in f n, g x ∂μ)
    (∑' (n : ℕ), ∫ (x : Ω) in f n, limitProcess (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) ℱ μ x ∂μ)

Tactic:
exact tsum_congr fun n => heq _ (measure_lt_top _ _)

Premises used: tsum_congr, MeasureTheory.measure_lt_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - g) 1 μ) atTop (𝓝 0)

Tactic:
tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top
    (fun n => (stronglyMeasurable_condExp.mono (ℱ.le n)).aestronglyMeasurable)
    (memLp_one_iff_integrable.2 hg) hg.uniformIntegrable_condExp_filtration.2.1
    (tendstoInMeasure_of_tendsto_ae
      (fun n => (stronglyMeasurable_condExp.mono (ℱ.le n)).aestronglyMeasurable)
      (hg.tendsto_ae_condExp hgmeas))

Premises used: Iff.mpr, le_rfl, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.tendsto_ae_condExp, And.right, And.left, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le, MeasureTheory.Integrable.uniformIntegrable_condExp_filtration, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, MeasureTheory.memLp_one_iff_integrable, MeasureTheory.tendstoInMeasure_of_tendsto_ae, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
⊢ ∀ᵐ (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
-- Module: Mathlib.Probability.Martingale.Convergence
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))
⊢ ∀ (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)
-- Module: Mathlib.Probability.Martingale.Convergence
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
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) i] a =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) i] a

Tactic:
rw [← ae_all_iff] at heq

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.Convergence
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
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))
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop
      (𝓝 (μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] x))

Tactic:
filter_upwards [heq, ht] with x hxeq hxt
-- Module: Mathlib.Probability.Martingale.Convergence
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 : Ω
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:
hxt.congr hxeq

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Probability.Martingale.Convergence
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 : Ω
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:
exact hxt.congr hxeq

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
⊢ 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
-- Module: Mathlib.Probability.Martingale.Convergence
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)
⊢ ∀ (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)
-- Module: Mathlib.Probability.Martingale.Convergence
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)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ)
    atTop (𝓝 0)

Tactic:
ht.congr fun n => eLpNorm_congr_ae ?_

Premises used: Filter.Tendsto.congr, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Probability.Martingale.Convergence
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)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
refine :
  ∀ (n : ℕ),
    μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
        μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
      μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ)
    atTop (𝓝 0)

Tactic:
refine ht.congr fun n => eLpNorm_congr_ae ?_

Premises used: Filter.Tendsto.congr, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Probability.Martingale.Convergence
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)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
n : ℕ
h :
  ∀ (x : Ω)
    (hxeq :
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x),
    (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
          μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
        x =
      (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) x
⊢ μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
      μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]

Tactic:
filter_upwards [heq n] with x hxeq
-- Module: Mathlib.Probability.Martingale.Convergence
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)
heq :
  ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
        μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
n : ℕ
x : Ω
hxeq :
  μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] x =
    μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x
⊢ (μ[μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n] | (↑ℱ : ℕ → MeasurableSpace Ω) n] -
        μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n])
      x =
    (μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n]) x

Tactic:
simp only [hxeq, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Martingale.condExp_ae_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
refine :
  μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})] f i

Tactic:
refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Martingale.condExp_ae_eq
-- Module: Mathlib.Probability.Martingale.OptionalSampling
Goal:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_3
inst_3 : LinearOrder ι
inst_4 : TopologicalSpace ι
inst_5 : OrderTopology ι
inst_6 : FirstCountableTopology ι
ℱ : Filtration ι m
inst_7 : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
i n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
inst_8 : SigmaFinite (μ.trim ⋯)
hin : i ≤ n
⊢ μ[f n | hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = (↑i : WithTop ι)})]
    μ[f n | (↑ℱ : ι → MeasurableSpace Ω) i]

Tactic:
condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i)
    (hτ.measurableSet_eq' i) fun t => ?_

Premises used: MeasureTheory.IsStoppingTime.measurableSpace_le, MeasureTheory.Filtration.le, MeasureTheory.IsStoppingTime.measurableSet_eq', MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_on