norm_sub_eq_lintegral — Mathlib

English

The L1 norm of a difference equals the lintegral of the pointwise norm of the difference.

Русский

Норма L1 разности равна линтегралу по точкам нормы разности.

LaTeX

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

Lean4

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

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