prod_norm_eq_add — Mathlib

English

For hp: 0 < p.toReal and f ∈ WithLp p (α × β), the norm equals the p‑norm of coordinate norms: ‖f‖ = (‖f.fst‖^{p.toReal} + ‖f.snd‖^{p.toReal})^{1/p.toReal}.

Русский

Для hp: 0 < p.toReal и f ∈ WithLp p (α × β) нормa равна p‑норме норм координат: \|f\| = (\|f.fst\|^{p.toReal} + \|f.snd\|^{p.toReal})^{1/p.toReal}.

LaTeX

$$$$\|f\| = \Big( \|f.fst\|^{\;p.toReal} + \|f.snd\|^{\;p.toReal} \Big)^{1 / p.toReal}$$$$

Lean4

theorem prod_norm_eq_add (hp : 0 < p.toReal) (f : WithLp p (α × β)) :
    ‖f‖ = (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ p.toReal) ^ (1 / p.toReal) :=
  let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

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