English
If f is AEMeasurable, then a.e.-measurable version of its NN Norm is AEMeasurable.
Русский
Если f A.E.-измерима, то a.e.-измеримая версия её NN-нормы является A.E.-измеримой.
LaTeX
$$$AEMeasurable f μ \\Rightarrow AEMeasurable (\\text{nnnorm} \\circ f) μ$$$
Lean4
theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty ι] {μ : Measure α} {f : ι → α → β}
{L : Filter ι} [L.IsCountablyGenerated] (hf : ∀ n, AEMeasurable (f n) μ)
(h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, Tendsto (fun n => f n x) L (𝓝 l)) :
∃ f_lim : α → β, Measurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) := by
classical
inhabit ι
rcases eq_or_neBot L with (rfl | hL)
· exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
let p : α → (ι → β) → Prop := fun x f' => ∃ l : β, Tendsto (fun n => f' n) L (𝓝 l)
have hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x := fun x hx => aeSeq.fun_prop_of_mem_aeSeqSet hf hx
have h_ae_eq : ∀ᵐ x ∂μ, ∀ n, aeSeq hf p n x = f n x := aeSeq.aeSeq_eq_fun_ae hf h_ae_tendsto
set f_lim : α → β := fun x =>
dite (x ∈ aeSeqSet hf p) (fun h => (hp_mem x h).choose) fun _ => (⟨f default x⟩ : Nonempty β).some
have hf_lim : ∀ x, Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x)) :=
by
intro x
simp only [aeSeq, f_lim]
split_ifs with h
· refine (hp_mem x h).choose_spec.congr fun n => ?_
exact (aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h n).symm
· exact tendsto_const_nhds
have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x)) :=
h_ae_eq.mono fun x hx => (hf_lim x).congr hx
have h_f_lim_meas : Measurable f_lim :=
measurable_of_tendsto_metrizable' L (aeSeq.measurable hf p) (tendsto_pi_nhds.mpr fun x => hf_lim x)
exact ⟨f_lim, h_f_lim_meas, h_ae_tendsto_f_lim⟩
