prod_norm_eq_add_idemFst — Mathlib

English

For general p with 1 ≤ p, and x ∈ WithLp p (α × β), the norm satisfies the relation with idemFst and idemSnd as a sum of p-powers in the appropriate real exponent.

Русский

Для общего p с 1 ≤ p и x ∈ WithLp p (α × β) норма удовлетворяет соотношению через idemFst и idemSnd как сумма p-й степени через соответствующий показатель.

LaTeX

$$$\|x\| = \bigl\{ \|\mathrm{idemFst}\,x\|^{p.toReal} + \|\mathrm{idemSnd}\,x\|^{p.toReal} \bigr\}^{1/p.toReal}$$$

Lean4

theorem prod_norm_eq_add_idemFst [Fact (1 ≤ p)] (hp : 0 < p.toReal) (x : WithLp p (α × β)) :
    ‖x‖ = (‖idemFst x‖ ^ p.toReal + ‖idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal) :=
  by
  rw [WithLp.prod_norm_eq_add hp, ← WithLp.norm_toLp_fst p α β x.1, ← WithLp.norm_toLp_snd p α β x.2]
  rfl

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