lintegral_enorm_of_nonneg — Mathlib

English

If f ≥ 0 (as a measurable Real-valued function), then the ENNReal integral of the norm equals the ENNReal integral of the real part via ofReal.

Русский

Пусть f ≥ 0; тогда интеграл нормы равен интегралу от Real через ofReal.

LaTeX

$$$f \\ge 0 \\Rightarrow \\int⁻ x, NNNorm.toENorm.enorm (f(x)) ∂μ = \\int⁻ x, ENNReal.ofReal(f(x)) ∂μ$$$

Lean4

theorem lintegral_enorm_of_nonneg {f : α → ℝ} (h_nonneg : 0 ≤ f) : ∫⁻ x, ‖f x‖ₑ ∂μ = ∫⁻ x, .ofReal (f x) ∂μ :=
  lintegral_enorm_of_ae_nonneg <| .of_forall h_nonneg

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