lintegral_enorm_neg — Mathlib

English

The lintegral of the EN-norm equals the lintegral of the edist to zero: ∫ ENNReal.ofReal ‖f‖ = ∫ edist(f, 0).

Русский

Линтеграл ENReal от ‖f‖ равен линтегралу edist(f, 0).

LaTeX

$$$ \\int^- a \\, \\mathrm{ENNReal.ofReal}(\\|f(a)\\|) \\, d\\mu(a) = \\int^- a \\, \\mathrm{edist}(f(a), 0) \\, d\\mu(a) $$$

Lean4

theorem lintegral_enorm_neg {f : α → β} : ∫⁻ a, ‖(-f) a‖ₑ ∂μ = ∫⁻ a, ‖f a‖ₑ ∂μ := by simp

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