lintegral_enorm_of_ae_nonneg — Mathlib

English

If f is almost everywhere nonnegative real-valued, then the ENNReal integral of ||f|| equals the ENNReal integral of ofReal f.

Русский

Пусть f неотрицательно почти всюду; тогда интеграл ||f|| равен интегралу ofReal(f).

LaTeX

$$$0 \\le^\\mathrm{a.e.}_{μ} f \\Rightarrow \\int⁻ x, NNNorm.toENorm.enorm (f(x)) ∂μ = \\int⁻ x, ENNReal.ofReal(f(x)) ∂μ$$$

Lean4

theorem lintegral_enorm_of_ae_nonneg {f : α → ℝ} (h_nonneg : 0 ≤ᵐ[μ] f) : ∫⁻ x, ‖f x‖ₑ ∂μ = ∫⁻ x, .ofReal (f x) ∂μ :=
  by
  apply lintegral_congr_ae
  filter_upwards [h_nonneg] with x hx
  rw [Real.enorm_eq_ofReal hx]

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