awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
ω : Ω
hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (hω.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))))

Tactic:
hω.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
ω : Ω
hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (hω.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))))

Tactic:
exact hω.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))

Tactic:
have hg' : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g' ω)) := by
    filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω
    simp_rw [g', dif_pos hω]
    exact hω.choose_spec
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
⊢ AEStronglyMeasurable g' (μ.trim hle)

Tactic:
have hg'm : AEStronglyMeasurable[⨆ n, ℱ n] g' (μ.trim hle) :=
    (@aemeasurable_of_tendsto_metrizable_ae' _ _ (⨆ n, ℱ n) _ _ _ _ _ _ _
      (fun n => ((hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩ : ℱ n ≤ ⨆ n, ℱ n)
        le_rfl).aemeasurable) hg').aestronglyMeasurable
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
hg'm : AEStronglyMeasurable g' (μ.trim hle)
obtain :
  ∀ (g : Ω → ℝ) (hgm : StronglyMeasurable g) (hae : g' =ᶠ[ae (μ.trim hle)] g),
    ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
obtain ⟨g, hgm, hae⟩ := hg'm
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
h :
  ∀ (ω : Ω) (hω : g' ω = g ω) (hg'ω : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))),
    Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
filter_upwards [hae, hg'] with ω hω hg'ω
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
ω : Ω
hω : g' ω = g ω
hg'ω : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
hω ▸ hg'ω

Premises used: Eq.rec
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
ω : Ω
hω : g' ω = g ω
hg'ω : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
exact hω ▸ hg'ω
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
have hg : ∀ᵐ ω ∂μ.trim hle, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) := by
    filter_upwards [hae, hg'] with ω hω hg'ω
    exact hω ▸ hg'ω
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
hg : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩

Premises used: MeasureTheory.measure_eq_zero_of_trim_eq_zero, And.intro, Exists.intro
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᶠ[ae (μ.trim hle)] g
hg : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
exact ⟨g, hgm, measure_eq_zero_of_trim_eq_zero hle hg⟩
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
p : ℝ≥0∞
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
⊢ MemLp (limitProcess f ℱ μ) p μ

Tactic:
memLp_limitProcess_of_eLpNorm_bdd
    (fun n => ((hf.stronglyMeasurable n).mono (ℱ.le n)).aestronglyMeasurable) hbdd

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Submartingale.stronglyMeasurable, MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
obtain :
  ∀ (R : ℝ≥0) (hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)),
    Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
obtain ⟨R, hR⟩ := hunif.2.2

Premises used: And.right
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ (n : ℕ), AEStronglyMeasurable (f n) μ

Tactic:
have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
    ((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)
hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hmeas
    (memLp_limitProcess_of_eLpNorm_bdd hmeas hR) hunif.2.1
    (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)

Premises used: le_rfl, MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd, And.right, And.left, MeasureTheory.Submartingale.ae_tendsto_limitProcess, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, MeasureTheory.tendstoInMeasure_of_tendsto_ae, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ (↑R : ℝ≥0∞)
hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
exact tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hmeas
    (memLp_limitProcess_of_eLpNorm_bdd hmeas hR) hunif.2.1
    (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)

Premises used: le_rfl, MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd, And.right, And.left, MeasureTheory.Submartingale.ae_tendsto_limitProcess, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, MeasureTheory.tendstoInMeasure_of_tendsto_ae, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))

Tactic:
let ⟨_, hR⟩ := hunif.2.2
  hf.ae_tendsto_limitProcess hR

Premises used: MeasureTheory.ae, _private.0.MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable.match_1, Filter.Eventually, nhds, Filter.atTop, And.right, Filter.Tendsto, MeasureTheory.Filtration.limitProcess, MeasureTheory.Submartingale.ae_tendsto_limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
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 : ℕ
rw : eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0
⊢ f n =ᶠ[ae μ] μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]

Tactic:
rw [← sub_ae_eq_zero, ← eLpNorm_eq_zero_iff (((hf.stronglyMeasurable n).mono (ℱ.le _)).sub
    (stronglyMeasurable_condExp.mono (ℱ.le _))).aestronglyMeasurable one_ne_zero]

Premises used: MeasureTheory.StronglyMeasurable.sub, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.sub_ae_eq_zero, MeasureTheory.eLpNorm_eq_zero_iff, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.Filtration.le, one_ne_zero, MeasureTheory.Martingale.stronglyMeasurable
-- Module: Mathlib.Probability.Martingale.Convergence
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 : ℕ
⊢ 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 _
-- Module: Mathlib.Probability.Martingale.Convergence
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 μ

Tactic:
fun m hm => eLpNorm_congr_ae ((condExp_sub (hf.integrable m) hg _).trans ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.Filtration.seq, MeasureTheory.condExp_sub, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Probability.Martingale.Convergence
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)
refine :
  ∀ (m : ℕ) (hm : m ≥ n),
    μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
      f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]
⊢ ∀ m ≥ n,
    eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ = eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ

Tactic:
refine fun m hm => eLpNorm_congr_ae ((condExp_sub (hf.integrable m) hg _).trans ?_)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Martingale.integrable, MeasureTheory.condExp_sub, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.Probability.Martingale.Convergence
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
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
⊢ μ[f m | (↑ℱ : ℕ → MeasurableSpace Ω) n] - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] =ᶠ[ae μ]
    f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]

Tactic:
filter_upwards [hf.2 n m hm] with x hx

Premises used: And.right
-- Module: Mathlib.Probability.Martingale.Convergence
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
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:
simp only [hx, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Convergence
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 μ

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]
-- Module: Mathlib.Probability.Martingale.Convergence
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)
hev :
  ∀ m ≥ n,
    eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ = eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
⊢ eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0

Tactic:
tendsto_nhds_unique (tendsto_atTop_of_eventually_const hev) ht

Premises used: tendsto_atTop_of_eventually_const, tendsto_nhds_unique
-- Module: Mathlib.Probability.Martingale.Convergence
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)
hev :
  ∀ m ≥ n,
    eLpNorm μ[f m - g | (↑ℱ : ℕ → MeasurableSpace Ω) n] 1 μ = eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ
⊢ eLpNorm (f n - μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ = 0

Tactic:
exact tendsto_nhds_unique (tendsto_atTop_of_eventually_const hev) ht

Premises used: tendsto_atTop_of_eventually_const, tendsto_nhds_unique
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : UniformIntegrable f 1 μ
n : ℕ
⊢ f n =ᶠ[ae μ] μ[limitProcess f ℱ μ | (↑ℱ : ℕ → MeasurableSpace Ω) n]

Tactic:
let ⟨_, hR⟩ := hbdd.2.2
  hf.eq_condExp_of_tendsto_eLpNorm ((memLp_limitProcess_of_eLpNorm_bdd hbdd.1 hR).integrable le_rfl)
    (hf.submartingale.tendsto_eLpNorm_one_limitProcess hbdd) n

Premises used: MeasureTheory.ae, _private.0.MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable.match_1, MeasureTheory.Martingale.submartingale, le_rfl, MeasureTheory.Filtration.seq, MeasureTheory.MemLp.integrable, Filter.EventuallyEq, MeasureTheory.condExp, MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd, And.right, And.left, MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess, MeasureTheory.Filtration.limitProcess, MeasureTheory.Martingale.eq_condExp_of_tendsto_eLpNorm
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
⊢ ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0

Tactic:
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.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
⊢ UniformIntegrable (β := ℝ) (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n]) 1 μ

Tactic:
have hunif : UniformIntegrable (fun n => μ[g | ℱ n]) 1 μ :=
    hg.uniformIntegrable_condExp_filtration
-- 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 μ
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))
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ μ[g | (↑ℱ : ℕ → MeasurableSpace Ω) n] x) atTop (𝓝 (g x))

Tactic:
obtain ⟨R, hR⟩ := hunif.2.2

Premises used: And.right
-- 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∞)
⊢ 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