p power of tsum le of tsum of p powers

Stream: maths

[Filippo A. E. Nuccio]

Given a function $f \colon \mathbb{N}\to \mathbb{R}$ and $0<p<1$, do we have that

$$\Vert \sum{}' f_n\Vert ^p \leq (\sum {}'\Vert f_n\Vert ^p)\quad?$$

@Heather Macbeth , may be you needed something like this for $\ell_p$-spaces?

[Heather Macbeth]

Good question ... There is docs#rpow_add_le_add_rpow for two arguments. To get it in general, you could prove for n arguments by induction, and then use the same methods as e.g. in docs#inner_le_Lp_mul_Lq_tsum to extend from finite to infinite sum.

[Heather Macbeth]

(Maybe let's see if @Rémy Degenne has seen it somewhere, too)

[Filippo A. E. Nuccio]

Yes, thanks! I think I can do this quite fast using something that @Johan Commelin has developed for LTE. I will try to do this and push it soon.