English
The nnnorm of the integral of an L1 function is bounded by the nnnorm of the function itself, in the NNReal sense.
Русский
nnnorm интеграла из L1‑функции ограничен nnnorm самой функции в смыслe NNReal.
LaTeX
$$$\\|\\int f\\|_{+} \\le \\|f\\|_{+}$$$
Lean4
theorem integral_eq_norm_posPart_sub (f : α →₁[μ] ℝ) : integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖ := by
-- Use `isClosed_property` and `isClosed_eq`
refine
@isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
(fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) (simpleFunc.denseRange one_ne_top)
(isClosed_eq ?_ ?_) ?_ f
· simp only [integral]
exact cont _
·
refine
Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
(continuous_norm.comp Lp.continuous_negPart)
-- Show that the property holds for all simple functions in the `L¹` space.
· intro s
norm_cast
exact SimpleFunc.integral_eq_norm_posPart_sub _
