English
If hp > 0 and f ∈ lp(E,p) and s is a finite set of indices, the p-th power of the norm of f equals the sum of the p-th powers of the norms of its coordinates over s, up to a telescoping relation with the remainder.
Русский
Пусть hp > 0, f ∈ lp(E,p), s конечное множество индексов; тогда сумма норм по координатам на s равна разности норм, возведённых в p-ю степень.
LaTeX
$$$0 < p^{\\toReal} \\implies \\|f\\|^{p.toReal} - \\|f - \\sum_{i\\in s} lp.single(p,i)(f(i))\\|^{p.toReal} = \\sum_{i\\in s} \\|f(i)\\|^{p.toReal}.$$$
Lean4
protected theorem norm_sub_norm_compl_sub_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal :=
by
refine ((hasSum_norm hp f).sub (hasSum_norm hp (f - ∑ i ∈ s, lp.single p i (f i)))).unique ?_
let F : α → ℝ := fun i => ‖f i‖ ^ p.toReal - ‖(f - ∑ i ∈ s, lp.single p i (f i)) i‖ ^ p.toReal
have hF : ∀ i ∉ s, F i = 0 := by
intro i hi
suffices ‖f i‖ ^ p.toReal - ‖f i - ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 by
simpa only [coeFn_sub, coeFn_sum, lp.coeFn_single, Pi.sub_apply, Finset.sum_apply, Finset.sum_pi_single, F] using
this
simp only [if_neg hi, sub_zero, sub_self]
have hF' : ∀ i ∈ s, F i = ‖f i‖ ^ p.toReal := by
intro i hi
simp only [F, coeFn_sum, lp.single_apply, if_pos hi, sub_self, coeFn_sub, Pi.sub_apply, Finset.sum_apply,
Finset.sum_pi_single, sub_eq_self]
simp [Real.zero_rpow hp.ne']
have : HasSum F (∑ i ∈ s, F i) := hasSum_sum_of_ne_finset_zero hF
rwa [Finset.sum_congr rfl hF'] at this
