English
For Realened p>0 the norm of a finite sum of single terms equals the sum of norms to the p-power, as in the previous norm-sum lemma.
Русский
Для положительного p верно равенство нормы конечной суммы через нормы отдельных членов в степенях p.
LaTeX
$$$\|\sum_{i\in s} \text{lp.single } p i (f_i)\|^{p.toReal} = \sum_{i\in s} \|f_i\|^{p.toReal}.$$$
Lean4
protected theorem norm_sum_single (hp : 0 < p.toReal) (f : ∀ i, E i) (s : Finset α) :
‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal :=
by
refine (hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_
simp only [lp.coeFn_single, coeFn_sum, Finset.sum_apply, Finset.sum_pi_single]
have h : ∀ i ∉ s, ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := fun i hi ↦ by simp [if_neg hi, Real.zero_rpow hp.ne']
have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal :=
by
intro i hi
rw [if_pos hi]
simpa [Finset.sum_congr rfl h'] using hasSum_sum_of_ne_finset_zero h
