lintegral_ofReal_le_lintegral_enorm

English

For a real-valued function f, the integral of |f| equals the integral of the ENNReal norm of f when integrating via the ofReal map.

Русский

Для вещественной функции f интеграл от |f| равен интегралу нормы ENNReal от f после отображения через ofReal.

LaTeX

$$$\\int⁻ x, \\lVert f(x) \\rVertₑ ∂μ = \\int⁻ x, \\text{ofReal}(f(x)) ∂μ$$$

Lean4

theorem lintegral_ofReal_le_lintegral_enorm (f : α → ℝ) : ∫⁻ x, ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ x, ‖f x‖ₑ ∂μ :=
  by
  simp_rw [← ofReal_norm_eq_enorm]
  refine lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_
  rw [Real.norm_eq_abs]
  exact le_abs_self (f x)

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