-- Mathlib/Probability/Martingale/Convergence.lean
theorem Martingale.eq_condExp_of_tendsto_eLpNorm {μ : Measure Ω} (hf : Martingale f ℱ μ)
    (hg : Integrable g μ) (hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)) (n : ℕ) :
    f n =ᵐ[μ] μ[g|ℱ n]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
hev : ∀ m ≥ n, eLpNorm (μ[f m - g|↑ℱ n]) 1 μ = eLpNorm (f n - μ[g|↑ℱ n]) 1 μ
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0

Tactic:
exact tendsto_nhds_unique (tendsto_atTop_of_eventually_const hev) ht

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ ∀ m ≥ n, eLpNorm (μ[f m - g|↑ℱ n]) 1 μ = eLpNorm (f n - μ[g|↑ℱ n]) 1 μ

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

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
⊢ μ[f m|↑ℱ n] - μ[g|↑ℱ n] =ᶠ[ae μ] f n - μ[g|↑ℱ n]

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
x : Ω
hx : (μ[f m|↑ℱ n]) x = f n x
⊢ (μ[f m|↑ℱ n] - μ[g|↑ℱ n]) x = (f n - μ[g|↑ℱ n]) x

Tactic:
simp only [hx, Pi.sub_apply]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 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 _

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ f n =ᶠ[ae μ] μ[g|↑ℱ 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]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
⊢ μ[f m|↑ℱ n] - μ[g|↑ℱ n] =ᶠ[ae μ] f n - μ[g|↑ℱ n]

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

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
m : ℕ
hm : m ≥ n
x : Ω
hx : (μ[f m|↑ℱ n]) x = f n x
⊢ (μ[f m|↑ℱ n] - μ[g|↑ℱ n]) x = (f n - μ[g|↑ℱ n]) x

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0

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]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
g : Ω → ℝ
μ : Measure Ω
hf : Martingale f ℱ μ
hg : Integrable g μ
hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)
n : ℕ
ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)
hev : ∀ m ≥ n, eLpNorm (μ[f m - g|↑ℱ n]) 1 μ = eLpNorm (f n - μ[g|↑ℱ n]) 1 μ
⊢ eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0