English
If f and g are integrable with μ, the edistance between their L1-images equals the integral of the pointwise edist: edist(toL1 f, toL1 g) = ∫ edist(f(a), g(a)) dμ.
Русский
Если f и g интегрируемы по μ, расстояние edist между их L1-образами равно интегралу по μ от точечного расстояния: edist(toL1 f, toL1 g) = ∫ edist(f(a), g(a)) dμ.
LaTeX
$$$ \\mathrm{edist}\\big( \\mathrm{toL1}(f), \\mathrm{toL1}(g) \\big) = \\int^- a \\, \\mathrm{edist}\\big( f(a), g(a) \\big) \\, d\\mu(a) $$$
Lean4
@[simp]
theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrable g μ) :
edist (hf.toL1 f) (hg.toL1 g) = ∫⁻ a, edist (f a) (g a) ∂μ :=
by
simp only [toL1, Lp.edist_toLp_toLp, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm, Pi.sub_apply, toReal_one,
ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]
simp [edist_eq_enorm_sub]
