English
In the real power version, the same finite-subset identity holds with p.toReal, yielding a relation between the norm of f minus partial sum and the sum of p-th power norms of coordinates.
Русский
В действительной версии то же тождество сохраняется: разность норм возводится в p.toReal и равна сумме норм в p-й степени по координатам на s.
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_compl_sum_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by
linarith [lp.norm_sub_norm_compl_sub_single hp f s]
