real_toNNReal — Mathlib

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]

Похожие утверждения