ofReal_norm_sub_eq_lintegral — Mathlib

English

For f,g in L1, the norm of their difference equals the lintegral of the pointwise norm of their difference.

Русский

Для f,g в L1 норма их разности равна линегралу нормы разности по точкам.

LaTeX

$$\|f - g\| = (∫⁻ x, \|f x - g x\|)∂μ$$

Lean4

/-- Computing the norm of a difference between two L¹-functions. Note that this is not a
  special case of `ofReal_norm_eq_lintegral` since `(f - g) x` and `f x - g x` are not equal
  (but only a.e.-equal). -/
theorem ofReal_norm_sub_eq_lintegral (f g : α →₁[μ] β) : ENNReal.ofReal ‖f - g‖ = ∫⁻ x, ‖f x - g x‖ₑ ∂μ :=
  by
  simp_rw [ofReal_norm_eq_lintegral, ← edist_zero_eq_enorm]
  apply lintegral_congr_ae
  filter_upwards [Lp.coeFn_sub f g] with _ ha
  simp only [ha, Pi.sub_apply]

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