instProdNormSMulClass — Mathlib

English

In the L1 case, the norm of x equals the sum of the norms of its projections: ||x|| = ||idemFst x|| + ||idemSnd x||.

Русский

В случае L1 норма x равна сумме норм его проекций: ||x|| = ||idemFst x|| + ||idemSnd x||.

LaTeX

$$$\|x\| = \|\mathrm{idemFst}\,x\| + \|\mathrm{idemSnd}\,x\|.$$$

Lean4

instance instProdNormSMulClass [SeminormedRing 𝕜] [Module 𝕜 α] [Module 𝕜 β] [NormSMulClass 𝕜 α] [NormSMulClass 𝕜 β] :
    NormSMulClass 𝕜 (WithLp p (α × β)) :=
  .of_nnnorm_smul fun c f => by
    rcases p.dichotomy with (rfl | hp)
    · simp only [← prod_nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
    · have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
      have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
      rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne', NNReal.mul_rpow, ←
        NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add, ← NNReal.mul_rpow, ← NNReal.mul_rpow,
        smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]

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