prod_norm_eq_idemFst_of_L1 — Mathlib

English

In the L1 case, the norm of x in WithLp 1 (α × β) equals the sum of the norms of its projections: ||x|| = ||idemFst x|| + ||idemSnd x||.

Русский

В случае L1 норма x в WithLp 1 (α × β) равна сумме норм его проекций: ||x|| = ||idemFst x|| + ||idemSnd x||.

LaTeX

$$$\|x\| = \|idemFst\,x\| + \|idemSnd\,x\|.$$$

Lean4

theorem prod_norm_eq_idemFst_of_L1 (x : WithLp 1 (α × β)) : ‖x‖ = ‖idemFst x‖ + ‖idemSnd x‖ :=
  by
  rw [prod_norm_eq_add_idemFst (lt_of_lt_of_eq zero_lt_one toReal_one.symm)]
  simp only [toReal_one, Real.rpow_one, ne_eq, one_ne_zero, not_false_eq_true, div_self]

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