Convexity properties of rpow

We prove basic convexity properties of the rpow function. The proofs are elementary and do not require calculus, and as such this file has only moderate dependencies.

Main declarations

• NNReal.strictConcaveOn_rpow, Real.strictConcaveOn_rpow: strict concavity of fun x ↦ x ^ p for p ∈ (0,1)
• NNReal.concaveOn_rpow, Real.concaveOn_rpow: concavity of fun x ↦ x ^ p for p ∈ [0,1]

Note that convexity for p > 1 can be found in Analysis.Convex.SpecificFunctions.Basic, which requires slightly less imports.

TODO

• Prove convexity for negative powers.

theorem NNReal.strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : StrictConcaveOn NNReal Set.univ fun (x : NNReal) => x ^ p

theorem NNReal.concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : ConcaveOn NNReal Set.univ fun (x : NNReal) => x ^ p

theorem NNReal.strictConcaveOn_sqrt : StrictConcaveOn NNReal Set.univ ⇑sqrt

theorem Real.strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : StrictConcaveOn ℝ (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem Real.concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : ConcaveOn ℝ (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem Real.strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) fun (x : ℝ) => √x