integral_norm_eq_lintegral_enorm — Mathlib

English

For a Bochner integrable f: α → P, the integral of the norm equals the lintegral of the ENNReal norm, i.e., ∫ ‖f‖ dμ equals the real part of the ENNReal integral of ‖f‖, establishing compatibility between the two integral notions.

Русский

Для интегрируемой функции f выполняется совпадение интеграла нормы и линтеграла нормы.

LaTeX

$$$\\int a, \\|f(a)\\|\\,d\\mu = \\int^- a, \\lVert f(a)\\rVert_e\\,d\\mu.~\\text{(in Real via }toReal\\text{)}$$$

Lean4

theorem integral_norm_eq_lintegral_enorm {P : Type*} [NormedAddCommGroup P] {f : α → P}
    (hf : AEStronglyMeasurable f μ) : ∫ x, ‖f x‖ ∂μ = (∫⁻ x, ‖f x‖ₑ ∂μ).toReal :=
  by
  rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]
  · simp_rw [ofReal_norm_eq_enorm]
  · filter_upwards; simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]

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