## Stream: Is there code for X?

### Topic: monotonicty of l^p norms

#### Andrew Souther (Jan 13 2021 at 19:07):

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 (Jan 13 2021 at 19:20):

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

#### Sebastien Gouezel (Jan 13 2021 at 19:27):

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

#### Heather Macbeth (Jan 13 2021 at 19:28):

But I think that's the opposite direction!

Ah, yes. Sorry!

#### Rémy Degenne (Jan 21 2021 at 13:25):

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

Last updated: May 07 2021 at 21:10 UTC