norm_eq_integral_norm — Mathlib

English

For f: α → H integrable, the L1 norm equals the integral of the pointwise norms: ‖f‖₁ = ∫ ‖f(x)‖ dμ.

Русский

Для интегрируемой функции f: α → H нормa L1 равна интегралу по мере от нормы функции: ‖f‖₁ = ∫ ‖f(x)‖ dμ.

LaTeX

$$$\\\\|f\\\\|_{L^1} = \\\\int a \\, \\\\|f(a)\\\\| \\, d\\\\mu$$$

Lean4

theorem norm_eq_integral_norm (f : α →₁[μ] H) : ‖f‖ = ∫ a, ‖f a‖ ∂μ :=
  by
  simp only [eLpNorm, eLpNorm'_eq_lintegral_enorm, ENNReal.toReal_one, ENNReal.rpow_one, Lp.norm_def, if_false,
    ENNReal.one_ne_top, one_ne_zero, _root_.div_one]
  rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall (by simp [norm_nonneg]))
      (Lp.aestronglyMeasurable f).norm]
  simp

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