dist_eq_sum — Mathlib

English

For 0 < p.toReal, the distance satisfies dist f g = (∑ dist(f_i,g_i)^{p.toReal})^{1/p.toReal}.

Русский

Для 0 < p.toReal расстояние удовлетворяет dist f g = (∑ dist(f_i,g_i)^{p.toReal})^{1/p.toReal}.

LaTeX

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

Lean4

theorem dist_eq_sum {p : ℝ≥0∞} (hp : 0 < p.toReal) (f g : PiLp p α) :
    dist f g = (∑ i, dist (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)

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