[Merged by Bors] - feat: Bernoulli's inequality for 0 < p < 1

[Parcly-Taxel]

Also substantially speed up some existing proofs in the p < 1 case.

---

[loefflerd]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5901374.
There were significant changes against commit 5fc4f86:

  Benchmark                                          Metric         Change
  ========================================================================
+ ~Mathlib.Analysis.Convex.SpecificFunctions.Basic   instructions   -42.3%

[loefflerd]

Not bad: the file now takes about half as long as before, despite having roughly twice as many theorems! Thanks for taking on this job. I'll try to find time to proofread it for style later today, then it should be good to go.

[loefflerd]

Umm, I just spotted something I should have realised much earlier.

There is a file Mathlib.Analysis.Convex.SpecificFunctions.Pow, which contains a theorem

lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) :
    StrictConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p := by

So we are just reinventing the wheel here. ☹️ I apologise for not having realised this first time around.

Perhaps the best way forward is the following. The Bernoulli inequality for p < 1 is a statement of interest in its own right, so I suggest keeping the proof you've written for that. But it might be best to replace your proof of strictConcaveOn_rpow, and its non-strict version, with a (hopefully much quicker) version deducing it from the existing NNReal version. This would have to live in Convex.SpecificFunctions.Pow, so I also suggest adding a comment to Convex.SpecificFunctions.Basic explicitly pointing out that the p < 1 case is treated elsewhere.

[Parcly-Taxel]

But it might be best to replace your proof of strictConcaveOn_rpow, and its non-strict version, with a (hopefully much quicker) version deducing it from the existing NNReal version. This would have to live in Convex.SpecificFunctions.Pow, so I also suggest adding a comment to Convex.SpecificFunctions.Basic explicitly pointing out that the p < 1 case is treated elsewhere.

The proof of Real.strictConcaveOn_rpow in Analysis.Convex.SpecificFunctions.Pow already goes through the NNReal version:

lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) :
    StrictConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p := by
  refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
  let x' : ℝ≥0 := ⟨x, hx⟩
  let y' : ℝ≥0 := ⟨y, hy⟩
  let a' : ℝ≥0 := ⟨a, by positivity⟩
  let b' : ℝ≥0 := ⟨b, by positivity⟩
  have hx' : (fun z => z ^ p) x = (fun z => z ^ p) x' := rfl
  have hy' : (fun z => z ^ p) y = (fun z => z ^ p) y' := rfl
  have hxy' : x' ≠ y' := Subtype.ne_of_val_ne hxy
  have hab' : a' + b' = 1 := by ext; simp [a', b', hab]
  rw [hx', hy']
  exact (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y')
    hxy' (mod_cast ha) (mod_cast hb) hab'

I think the better approach is to move the currently un-namespaced (strict)?ConvexOn_rpow to Analysis.Convex.SpecificFunctions.Pow (where (strict)?ConcaveOn_sqrt also lives), namespace it and prove it from a new NNReal version.

[loefflerd]

But it might be best to replace your proof of strictConcaveOn_rpow, and its non-strict version, with a (hopefully much quicker) version deducing it from the existing NNReal version. This would have to live in Convex.SpecificFunctions.Pow, so I also suggest adding a comment to Convex.SpecificFunctions.Basic explicitly pointing out that the p < 1 case is treated elsewhere.

The proof of Real.strictConcaveOn_rpow in Analysis.Convex.SpecificFunctions.Pow already goes through the NNReal version:

If this already exists in the other file, then there is even less for this PR to do.

I think the better approach is to move the currently un-namespaced (strict)?ConvexOn_rpow to Analysis.Convex.SpecificFunctions.Pow (where (strict)?ConcaveOn_sqrt also lives), namespace it and prove it from a new NNReal version.

The reasons for not doing that are very clearly explained in the existing code. The file Analysis.Convex.SpecificFunctions.Pow needs more imports than Analysis.Convex.SpecificFunctions.Basic does. Because strictConvexOn_rpow is foundational for a whole load of analysis / measure theory code (anything involving L^p spaces), it is important to prove it with minimal imports; but this is not true of the concavity result for p < 1 which has far fewer applications.

[loefflerd]

LGTM. Please update the title of this PR to match the content – when that's done I'll ping the maintainers.

[Parcly-Taxel]

LGTM. Please update the title of this PR to match the content – when that's done I'll ping the maintainers.

It is done now?

[loefflerd]

I added a little more explanation to the header string. Code LGTM.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style