nnnorm_toLp_inr — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem nnnorm_toLp_inr (y : β) : ‖toLp p ((0 : α), y)‖₊ = ‖y‖₊ := 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]

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