English
A limit (over a general filter) of measurable ENNReal-valued functions is measurable.
Русский
Предел последовательности измеримых функций ENNReal есть измеримая функция.
LaTeX
$$$\text{measurable_of_tendsto}$$$
Lean4
/-- A limit (over a general filter) of a.e.-measurable `ℝ≥0∞`-valued functions is
a.e.-measurable. -/
theorem aemeasurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} {μ : Measure α} (u : Filter ι) [NeBot u]
[IsCountablyGenerated u] (hf : ∀ i, AEMeasurable (f i) μ) (hlim : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))) :
AEMeasurable g μ := by
rcases u.exists_seq_tendsto with ⟨v, hv⟩
have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n ↦ hf (v n)
set p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
have hp : ∀ᵐ x ∂μ, p x fun n ↦ f (v n) x := by filter_upwards [hlim] with x hx using hx.comp hv
classical
set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p) (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
· unfold aeSeqLim
simp_rw [aeSeq]
split_ifs with hx
· simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
· exact tendsto_const_nhds
·
exact
(ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some) (aeSeqSet h'f p)
(aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
