-- Mathlib/Probability/Martingale/Convergence.lean
theorem Integrable.tendsto_ae_condExp (hg : Integrable g μ)
    (hgmeas : StronglyMeasurable[⨆ n, ℱ n] g) :
    ∀ᵐ x ∂μ, Tendsto (fun n => (μ[g|ℱ n]) x) atTop (𝓝 (g x))

Proof state:
case intro.basic
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s✝ : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
s : Set Ω
hs : s ∈ {s | ∃ n, MeasurableSet s}
x✝ : μ s < ⊤
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ

Tactic:
rcases hs with ⟨n, hn⟩

Result:
case intro.basic.intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s✝ : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
s : Set Ω
x✝ : μ s < ⊤
n : ℕ
hn : MeasurableSet s
⊢ ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ 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]

Result:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
⊢ g =ᶠ[ae μ] limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))

Tactic:
have hlimint : Integrable (ℱ.limitProcess (fun n => μ[g|ℱ n]) μ) μ :=
  (memLp_limitProcess_of_eLpNorm_bdd hunif.1 hR).integrable le_rfl

Result:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 (g x))

Proof state:
case intro.compl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
x✝ : μ tᶜ < ⊤
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ

Tactic:
have hgeq := @setIntegral_compl _ _ (⨆ n, ℱ n) _ _ _ _ _ htmeas (hg.trim hle hgmeas)

Result:
case intro.compl
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
t : Set Ω
htmeas : MeasurableSet t
ht : μ t < ⊤ → ∫ (x : Ω) in t, g x ∂μ = ∫ (x : Ω) in t, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
x✝ : μ tᶜ < ⊤
hgeq : ∫ (x : Ω) in tᶜ, g x ∂μ.trim hle = ∫ (x : Ω), g x ∂μ.trim hle - ∫ (x : Ω) in t, g x ∂μ.trim hle
⊢ ∫ (x : Ω) in tᶜ, g x ∂μ = ∫ (x : Ω) in tᶜ, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → (μ[g|↑ℱ n]) x = (μ[limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ|↑ℱ n]) x

Tactic:
filter_upwards [(martingale_condExp g ℱ μ).ae_eq_condExp_limitProcess hunif n] with x hx _

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
n : ℕ
s : Set Ω
hs : MeasurableSet s
x : Ω
hx : (μ[g|↑ℱ n]) x = (μ[limitProcess (fun i => μ[g|↑ℱ i]) ℱ μ|↑ℱ n]) x
a✝ : x ∈ s
⊢ (μ[g|↑ℱ n]) x = (μ[limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ|↑ℱ n]) x

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n => μ[g|↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n => μ[g|↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n => μ[g|↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x => (μ[g|↑ℱ n]) x) ℱ μ x ∂μ
s : Set Ω
hs : MeasurableSet s
x✝ : μ s < ⊤
⊢ IsPiSystem (⋃ i, {x | MeasurableSet x})

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

Result:
no goals