English
If two sequences fs and gs converge a.e. with dominated bounds and every n has μ[fs_n|m] = μ[gs_n|m], then the limits of condExpL1 hm μ fs and gs are a.e. equal.
Русский
Если два последовательности сходятся a.e. и удовлетворяют общим ограничениями, а для каждого n имеют равенство условного ожидания, то пределы condExpL1 для них совпадают a.e.
LaTeX
$$$\forall n, \mu[fs_n|m] =^{\mathrm{ae}}\mu[gs_n|m] \Rightarrow \mu[f|m] =^{\mathrm{ae}}\mu[g|m]$$$
Lean4
/-- If two sequences of functions have a.e. equal conditional expectations at each step, converge
and verify dominated convergence hypotheses, then the conditional expectations of their limits are
a.e. equal. -/
theorem tendsto_condExp_unique (fs gs : ℕ → α → E) (f g : α → E) (hfs_int : ∀ n, Integrable (fs n) μ)
(hgs_int : ∀ n, Integrable (gs n) μ) (hfs : ∀ᵐ x ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x)))
(hgs : ∀ᵐ x ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))) (bound_fs : α → ℝ)
(h_int_bound_fs : Integrable bound_fs μ) (bound_gs : α → ℝ) (h_int_bound_gs : Integrable bound_gs μ)
(hfs_bound : ∀ n, ∀ᵐ x ∂μ, ‖fs n x‖ ≤ bound_fs x) (hgs_bound : ∀ n, ∀ᵐ x ∂μ, ‖gs n x‖ ≤ bound_gs x)
(hfg : ∀ n, μ[fs n|m] =ᵐ[μ] μ[gs n|m]) : μ[f|m] =ᵐ[μ] μ[g|m] :=
by
by_cases hm : m ≤ m₀; swap; · simp_rw [condExp_of_not_le hm]; rfl
by_cases hμm : SigmaFinite (μ.trim hm); swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl
refine (condExp_ae_eq_condExpL1 hm f).trans ((condExp_ae_eq_condExpL1 hm g).trans ?_).symm
rw [← Lp.ext_iff]
have hn_eq : ∀ n, condExpL1 hm μ (gs n) = condExpL1 hm μ (fs n) :=
by
intro n
ext1
refine (condExp_ae_eq_condExpL1 hm (gs n)).symm.trans ((hfg n).symm.trans ?_)
exact condExp_ae_eq_condExpL1 hm (fs n)
have hcond_fs : Tendsto (fun n => condExpL1 hm μ (fs n)) atTop (𝓝 (condExpL1 hm μ f)) :=
tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hfs_int n).1) h_int_bound_fs hfs_bound hfs
have hcond_gs : Tendsto (fun n => condExpL1 hm μ (gs n)) atTop (𝓝 (condExpL1 hm μ g)) :=
tendsto_condExpL1_of_dominated_convergence hm _ (fun n => (hgs_int n).1) h_int_bound_gs hgs_bound hgs
exact tendsto_nhds_unique_of_eventuallyEq hcond_gs hcond_fs (Eventually.of_forall hn_eq)
