-- Mathlib/Probability/Martingale/Convergence.lean
theorem tendsto_eLpNorm_condExp (g : Ω → ℝ) :
    Tendsto (fun n => eLpNorm (μ[g|ℱ n] - μ[g|⨆ n, ℱ n]) 1 μ) atTop (𝓝 0)

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
x : Ω
hxeq : (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x = (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x

Tactic:
simp only [hxeq, Pi.sub_apply]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
⊢ μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n] =ᶠ[ae μ] μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]

Tactic:
filter_upwards [heq n] with x hxeq

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
x : Ω
hxeq : (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x = (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) x

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
⊢ Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ 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

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)

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

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
n : ℕ
⊢ μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n] =ᶠ[ae μ] μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)

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)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : Tendsto (fun n => eLpNorm (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ Tendsto (fun n => eLpNorm (μ[g|↑ℱ n] - μ[g|⨆ n, ↑ℱ n]) 1 μ) atTop (𝓝 0)