edist_eq_sum — Mathlib

English

If 0 < p.toReal, then edist(f,g) = (∑_i edist(f_i,g_i)^{p.toReal})^{1/p.toReal}.

Русский

Если 0 < p.toReal, тогда edist(f,g) = (∑_i edist(f_i,g_i)^{p.toReal})^{1/p.toReal}.

LaTeX

$$$$edist(f,g)=\\left(\\sum_i edist(f_i,g_i)^{p^{\\mathrm{toReal}}}\\right)^{1/p^{\\mathrm{toReal}}}$$$$

Lean4

theorem edist_eq_sum {p : ℝ≥0∞} (hp : 0 < p.toReal) (f g : PiLp p β) :
    edist f g = (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) :=
  let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

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