dist_eq_integral_dist — Mathlib

English

The L1 distance between Bochner integrable functions f, g equals the integral of pointwise distances: dist(f,g) = ∫ dist(f(x), g(x)) dμ.

Русский

Расстояние L1 между функциями Бо́хнера f и g равно интегралу по точкам расстояния между значениями: dist(f,g) = ∫ dist(f(x), g(x)) dμ.

LaTeX

$$$\\\\operatorname{dist}(f,g) = \\\\int a \\, dist(f(a), g(a)) \\, d\\\\mu$$$

Lean4

theorem dist_eq_integral_dist (f g : α →₁[μ] H) : dist f g = ∫ a, dist (f a) (g a) ∂μ :=
  by
  simp only [dist_eq_norm, L1.norm_eq_integral_norm]
  exact integral_congr_ae <| (Lp.coeFn_sub _ _).fun_comp norm

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