Zulip Chat Archive

Stream: Is there code for X?

Topic: monotonicty of l^p norms


view this post on Zulip Andrew Souther (Jan 13 2021 at 19:07):

Does mathlib have a proof for the monotonicity of p\ell^p norms in finite dimension? Something like this inequality:
(xnq)1/q(xnp)1/p(\sum |x_n|^q)^{1/q} \leq (\sum |x_n|^p)^{1/p} for pqp \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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Jan 13 2021 at 19:27):

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

view this post on Zulip Heather Macbeth (Jan 13 2021 at 19:28):

But I think that's the opposite direction!

view this post on Zulip Sebastien Gouezel (Jan 13 2021 at 19:29):

Ah, yes. Sorry!

view this post on Zulip 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