English
Let p = n be a positive integer and β be a family of normed additively commutative groups indexed by ι. For any f in the product space PiLp p β, the p-norm is given by the standard finite- dimensional formula: the norm of f is (∑_{i ∈ ι} ‖f(i)‖^n)^{1/n}. In particular, when p = n, this is the usual ℓ^n-norm on the finite family.
Русский
Пусть p = n является положительным целым; пусть β = (β_i) и индексный множитель i пробегает по конечному множеству ι. Для любого f в пространстве PiLp p β норма p задаётся обычной конечномерной формулой: ‖f‖ = (∑_i ‖f(i)‖^n)^{1/n}. В частности, при p = n это обычная ℓ^n-норма на склейке по i.
LaTeX
$$$\|f\| = \left( \sum_{i\in ι} \|f(i)\|^{n} \right)^{1/n}, \quad p=n\in\mathbb{N}_{>0}, \; f:\; ι \to β_i,$$$
Lean4
theorem norm_eq_of_nat {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (n : ℕ) (h : p = n)
(f : PiLp p β) : ‖f‖ = (∑ i, ‖f i‖ ^ 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, norm_eq_sum this]
