monotonicty of l^p norms

Stream: Is there code for X?

[Andrew Souther]

Does mathlib have a proof for the monotonicity of $\ell^p$ norms in finite dimension? Something like this inequality:
$(\sum |x_n|^q)^{1/q} \leq (\sum |x_n|^p)^{1/p}$ for $p \leq q$.

Or in Lean, it may look like this:

example {ι : Type*} (s : finset ι) (f : ι → ℝ≥0) {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) :
  (∑ (i : ι) in s, f i ^ q) ^ (1 / q) ≤ (∑ (i : ι) in s, f i ^ p) ^ (1 / p) :=
sorry

[Ruben Van de Velde]

I'd start looking around https://leanprover-community.github.io/mathlib_docs/analysis/mean_inequalities.html

[Sebastien Gouezel]

We have docs#ℒp_space.snorm_le_snorm_of_exponent_le on probability spaces.

[Heather Macbeth]

But I think that's the opposite direction!

[Sebastien Gouezel]

Ah, yes. Sorry!

[Rémy Degenne]

I proved it for a sum of two terms in #5828. See rpow_add_rpow_le.