nnnorm_toLp_inl — Mathlib

English

For every p with 1 ≤ p and vectors x in α, the Lp-norm of the injection (x, 0) from α to α × β matches the original norm of x: ||toLp p (x,0)||_+ = ||x||_+.

Русский

Для каждого p с 1 ≤ p и вектора x из α норма Lp инекции (x, 0) в α × β совпадает с нормой x: ||toLp p (x,0)||_+ = ||x||_+.

LaTeX

$$$\|toLp(p)(x,0)\|_+ = \|x\|_+.$$$

Lean4

@[simp]
theorem nnnorm_toLp_inl (x : α) : ‖toLp p (x, (0 : β))‖₊ = ‖x‖₊ := by
  induction p generalizing hp with
  | top => simp [prod_nnnorm_eq_sup]
  | coe p =>
    have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
    simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

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