ofReal_integral_norm_eq_lintegral_enorm

English

For a Bochner integrable f: α → P, the real integral of the norm equals the lintegral of the ENNReal norm, confirming equality between these two representations of the total size of f.

Русский

Для интегрируемой по Бо́хнеру f выполняется равенство интеграла нормы и линегра́ла нормы.

LaTeX

$$$\\int a, \\|f(a)\\|\\,d\\mu = \\operatorname{toReal}\\left( \\int^- a, \\lVert f(a)\\rVert_e \\ d\\mu \\right)$$$

Lean4

theorem ofReal_integral_norm_eq_lintegral_enorm {P : Type*} [NormedAddCommGroup P] {f : α → P} (hf : Integrable f μ) :
    ENNReal.ofReal (∫ x, ‖f x‖ ∂μ) = ∫⁻ x, ‖f x‖ₑ ∂μ :=
  by
  rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal]
  exact lt_top_iff_ne_top.mp (hasFiniteIntegral_iff_enorm.mpr hf.2)

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