x^p is concave for 0 <= p <= 1

Stream: Is there code for X?

[Johan Commelin]

Does mathlib know that x^p is concave for 0 <= p <= 1 (real powers)?

[Johan Commelin]

I found docs#convex_on_rpow which gives convexity for 1 <= p

[Kevin Buzzard]

Can you use the fact that $x\mapsto x^p$ is the inverse of $x\mapsto x^{1/p}$?

[Johan Commelin]

let me see if those pieces of the puzzle are all there.

[Johan Commelin]

I've never done anything with concave functions in mathlib before

[Johan Commelin]

There's almost no mention of inv in analysis.convex.basic

[Mario Carneiro]

I think you only need to know that inv is antitone

[Johan Commelin]

Right, so some lemma about such compositions

[Johan Commelin]

I'll play around a bit more

[Yaël Dillies]

Johan Commelin said:

There's almost no mention of inv in analysis.convex.basic

analysis.convex.function :smirk:

[Johan Commelin]

We have an enormous amount on lp-stuff. Do we know that $\|x\|^p$ satisfies the triangle inequality for $p \le 1$?
@Heather Macbeth @Rémy Degenne

[Eric Wieser]

isn't there an instance on that for docs#pi_Lp? (edit: docs#pi_Lp.pseudo_emetric_space)

[Sebastien Gouezel]

We have docs#ennreal.rpow_add_le_add_rpow