prod_norm_eq_of_nat — Mathlib

English

For α,β normed spaces, if p = n is a natural number, then the Lp-norm of f ∈ WithLp p (α × β) equals (‖f.fst‖^n + ‖f.snd‖^n)^(1/n).

Русский

Для нормированных пространств α,β: если p = n, натуральное число, тогда нормa Lp(f) равна (‖f.fst‖^n + ‖f.snd‖^n)^{1/n}.

LaTeX

$$$\|f\| = (\|f.fst\|^n + \|f.snd\|^n)^{1/n}$$$

Lean4

theorem prod_norm_eq_of_nat [Norm α] [Norm β] (n : ℕ) (h : p = n) (f : WithLp p (α × β)) :
    ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / (n : ℝ)) :=
  by
  have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)
  simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast, prod_norm_eq_add this]

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