prod_nnnorm_eq_of_L2 — Mathlib

English

For x ∈ WithLp 2 (α × β), the NN-norm also satisfies the L2-Pythagorean relation: ‖x‖₊ = (‖x.fst‖₊^2 + ‖x.snd‖₊^2)^(1/2).

Русский

Для x ∈ WithLp 2 (α × β) NN-норма удовлетворяет тождеству L2-Пифагора: ‖x‖₊ = (‖x.fst‖₊^2 + ‖x.snd‖₊^2)^(1/2).

LaTeX

$$$\|x\|_{nn} = \sqrt{\|x_{\mathrm{fst}}\|_{nn}^2 + \|x_{\mathrm{snd}}\|_{nn}^2}$$$

Lean4

theorem prod_nnnorm_eq_of_L2 (x : WithLp 2 (α × β)) : ‖x‖₊ = NNReal.sqrt (‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact prod_norm_eq_of_L2 x

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