English
Let f be a function with MemLp f p μ and f be StronglyMeasurable, with p ≠ 0 and p ≠ ∞. Then f is FinStronglyMeasurable with respect to μ.
Русский
Пусть f удовлетворяет MemLp f p μ и сильно измерима; при этом p ≠ 0 и p ≠ ∞. Тогда f имеет конечную сильномерируемость относительно μ.
LaTeX
$$$\text{MemLp}(f,p,\mu) \land \text{StronglyMeasurable}(f) \land p \neq 0 \land p \neq \infty \Longrightarrow \text{FinStronglyMeasurable}(f,\mu)$$$
Lean4
theorem finStronglyMeasurable_of_stronglyMeasurable (hf : MemLp f p μ) (hf_meas : StronglyMeasurable f)
(hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) : FinStronglyMeasurable f μ :=
by
borelize G
haveI : SeparableSpace (Set.range f ∪ {0} : Set G) := hf_meas.separableSpace_range_union_singleton
let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)
refine ⟨fs, ?_, ?_⟩
· have h_fs_Lp : ∀ n, MemLp (fs n) p μ := SimpleFunc.memLp_approxOn_range hf_meas.measurable hf
exact fun n => (fs n).measure_support_lt_top_of_memLp (h_fs_Lp n) hp_ne_zero hp_ne_top
· intro x
apply SimpleFunc.tendsto_approxOn
apply subset_closure
simp
