English
If f is integrable, then the function x ↦ (f(x))^{toNNReal} considered in real numbers is integrable.
Русский
Если f интегрируема, то x ↦ (f(x))^{toNNReal} как функция в вещественных числах интегрируема.
LaTeX
$$$\\text{Integrable } f\\mu\\Rightarrow \\text{Integrable } (x\\mapsto (f(x))^{toNNReal}:\\mathbb{R})\\mu$$$
Lean4
@[fun_prop]
theorem real_toNNReal {f : α → ℝ} (hf : Integrable f μ) : Integrable (fun x => ((f x).toNNReal : ℝ)) μ :=
by
refine ⟨by fun_prop, ?_⟩
rw [hasFiniteIntegral_iff_norm]
refine lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)
apply lintegral_mono
intro x
simp [abs_le, le_abs_self]