From 9f245402d1d98435ad8544197660dfe0ada42af8 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Mon, 26 Feb 2024 14:47:26 +0800
Subject: [PATCH 1/5] feat: strict concavity of `x ^ p` when `0 < p < 1`

---
 .../Convex/SpecificFunctions/Basic.lean       | 105 ++++++++++++++++--
 1 file changed, 97 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 45f16125ae68d..919a26bba195d 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -19,17 +19,14 @@ In this file we prove that the following functions are convex or strictly convex
   $(0, +∞)$ and $(-∞, 0)$ respectively.
 * `convexOn_rpow`, `strictConvexOn_rpow` : For `p : ℝ`, `fun x ↦ x ^ p` is convex on $[0, +∞)$ when
   `1 ≤ p` and strictly convex when `1 < p`.
+* `concaveOn_rpow`, `strictConcaveOn_rpow` : For `p : ℝ`, `fun x ↦ x ^ p` is concave on $[0, +∞)$
+  when `0 ≤ p ≤ 1` and strictly concave when `0 < p < 1`.
 
 The proofs in this file are deliberately elementary, *not* by appealing to the sign of the second
-derivative.  This is in order to keep this file early in the import hierarchy, since it is on the
+derivative. This is in order to keep this file early in the import hierarchy, since it is on the
 path to Hölder's and Minkowski's inequalities and after that to Lp spaces and most of measure
 theory.
 
-## TODO
-
-For `p : ℝ`, prove that `fun x ↦ x ^ p` is concave when `0 ≤ p ≤ 1` and strictly concave when
-`0 < p < 1`.
-
 ## See also
 
 `Analysis.Convex.Mul` for convexity of `x ↦ x ^ n``
@@ -147,7 +144,47 @@ theorem one_add_mul_self_le_rpow_one_add {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp
   exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le
 #align one_add_mul_self_le_rpow_one_add one_add_mul_self_le_rpow_one_add
 
-/- For `p : ℝ` with `1 < p`, `fun x ↦ x ^ p` is strictly convex on $[0, +∞)$.
+/-- **Bernoulli's inequality** for real exponents, strict version: for `0 < p < 1` and `-1 ≤ s`,
+with `s ≠ 0`, we have `(1 + s) ^ p < 1 + p * s`. -/
+theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p)
+    (hp2 : p < 1) : (1 + s) ^ p < 1 + p * s := by
+  rcases eq_or_lt_of_le hs with (rfl | hs)
+  · have : p ≠ 0 := by positivity
+    simpa [zero_rpow this]
+  have hs1 : 0 < 1 + s := by linarith
+  rcases le_or_lt (1 + p * s) 0 with hs2 | hs2
+  · nlinarith
+  rw [rpow_def_of_pos hs1, ← exp_log hs2]
+  apply exp_strictMono
+  have hs3 : 1 + s ≠ 1 := by contrapose! hs'; linarith
+  have hs4 : 1 + p * s ≠ 1 := by contrapose! hs'; nlinarith
+  cases' lt_or_gt_of_ne hs' with hs' hs'
+  · rw [← lt_div_iff hp1, ← div_lt_div_right_of_neg hs']
+    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
+    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1
+    · field_simp
+    · field_simp
+    · nlinarith
+  · rw [← lt_div_iff hp1, ← div_lt_div_right hs']
+    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
+    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1
+    · field_simp
+    · field_simp
+    · nlinarith
+
+/-- **Bernoulli's inequality** for real exponents, non-strict version: for `0 ≤ p ≤ 1` and `-1 ≤ s`
+we have `(1 + s) ^ p ≤ 1 + p * s`. -/
+theorem rpow_one_add_le_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
+    (1 + s) ^ p ≤ 1 + p * s := by
+  rcases eq_or_lt_of_le hp1 with (rfl | hp1)
+  · simp
+  rcases eq_or_lt_of_le hp2 with (rfl | hp2)
+  · simp
+  by_cases hs' : s = 0
+  · simp [hs']
+  exact (rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le
+
+/-- For `p : ℝ` with `1 < p`, `fun x ↦ x ^ p` is strictly convex on $[0, +∞)$.
 
 We give an elementary proof rather than using the second derivative test, since this lemma is
 needed early in the analysis library. -/
@@ -198,6 +235,59 @@ theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : 
   exact (strictConvexOn_rpow hp).convexOn
 #align convex_on_rpow convexOn_rpow
 
+/-- For `p : ℝ` with `0 < p < 1`, `fun x ↦ x ^ p` is strictly concave on $[0, +∞)$.
+
+We give an elementary proof rather than using the second derivative test, since this lemma is
+needed early in the analysis library. -/
+theorem strictConcaveOn_rpow {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
+    StrictConcaveOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+  apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ici (0 : ℝ))
+  rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
+  have hy : 0 < y := by linarith
+  have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
+  have H1 : y ^ (p - 1 + 1) = y ^ (p - 1) * y := rpow_add_one hy.ne' _
+  ring_nf at H1
+  trans p * y ^ (p - 1)
+  · have hyz' : 0 < z - y := by linarith only [hyz]
+    have hyz'' : 1 < z / y := by rwa [one_lt_div hy]
+    have hyz''' : 0 < z / y - 1 := by linarith only [hyz'']
+    have hyz'''' : -1 ≤ z / y - 1 := by linarith only [hyz'']
+    have : (1 + (z / y - 1)) ^ p - 1 < p * (z / y - 1) := by
+      linarith [rpow_one_add_lt_one_add_mul_self hyz'''' hyz'''.ne' hp1 hp2]
+    rw [div_lt_iff hyz', ← div_lt_div_right hy']
+    convert this using 1
+    · have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _
+      ring_nf at H ⊢
+      field_simp at H ⊢
+      linear_combination -H
+    · ring_nf at H1 ⊢
+      field_simp at H1 ⊢
+      linear_combination p * (y - z) * y ^ p * H1
+  · have h3 : 0 < y - x := by linarith only [hxy]
+    have hyx'' : x / y < 1 := by rwa [div_lt_one hy]
+    have hyx''' : x / y - 1 < 0 := by linarith only [hyx'']
+    have hyx'''' : 0 ≤ x / y := by positivity
+    have hyx''''' : -1 ≤ x / y - 1 := by linarith only [hyx'''']
+    have : -p * (x / y - 1) < 1 - (1 + (x / y - 1)) ^ p := by
+      linarith [rpow_one_add_lt_one_add_mul_self hyx''''' hyx'''.ne hp1 hp2]
+    rw [lt_div_iff h3, ← div_lt_div_right hy']
+    convert this using 1
+    · ring_nf at H1 ⊢
+      field_simp
+      linear_combination p * (-y + x) * H1
+    · have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _
+      ring_nf at H ⊢
+      field_simp at H ⊢
+      linear_combination H
+
+theorem concaveOn_rpow {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
+    ConcaveOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+  rcases eq_or_lt_of_le hp1 with (rfl | hp1)
+  · simpa using concaveOn_const (c := 1) (convex_Ici _)
+  rcases eq_or_lt_of_le hp2 with (rfl | hp2)
+  · simpa using concaveOn_id (convex_Ici _)
+  exact (strictConcaveOn_rpow hp1 hp2).concaveOn
+
 theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by
   refine' ⟨convex_Iio _, _⟩
   rintro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
@@ -209,7 +299,6 @@ theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by
     _ < log (a • -x + b • -y) := (strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab)
     _ = log (-(a • x + b • y)) := by congr 1; simp only [Algebra.id.smul_eq_mul]; ring
     _ = _ := by rw [log_neg_eq_log]
-
 #align strict_concave_on_log_Iio strictConcaveOn_log_Iio
 
 namespace Real

From 1b9a0bf0cc4ddaf8a1c776756d9b1d7181cebd12 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Sun, 24 Mar 2024 13:12:21 +0800
Subject: [PATCH 2/5] "Sixths-of-proofs"

---
 .../Convex/SpecificFunctions/Basic.lean       | 181 +++++++-----------
 1 file changed, 71 insertions(+), 110 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 919a26bba195d..3957593f0dff4 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -103,34 +103,28 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
 `s ≠ 0`, we have `1 + p * s < (1 + s) ^ p`. -/
 theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp : 1 < p) :
     1 + p * s < (1 + s) ^ p := by
+  have hp' : 0 < p := zero_lt_one.trans hp
   rcases eq_or_lt_of_le hs with (rfl | hs)
-  · have : p ≠ 0 := by positivity
-    simpa [zero_rpow this]
-  have hs1 : 0 < 1 + s := by linarith
+  · rwa [add_right_neg, zero_rpow hp'.ne', mul_neg, mul_one, add_neg_lt_iff_lt_add, zero_add]
+  have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
   rcases le_or_lt (1 + p * s) 0 with hs2 | hs2
   · exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
+  have hs3 : 1 + s ≠ 1 := hs' ∘ add_right_eq_self.mp
+  have hs4 : 1 + p * s ≠ 1 := by
+    contrapose! hs'; rwa [add_right_eq_self, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
   rw [rpow_def_of_pos hs1, ← exp_log hs2]
   apply exp_strictMono
-  have hp : 0 < p := by positivity
-  have hs3 : 1 + s ≠ 1 := by contrapose! hs'; linarith
-  have hs4 : 1 + p * s ≠ 1 := by contrapose! hs'; nlinarith
   cases' lt_or_gt_of_ne hs' with hs' hs'
-  · rw [← div_lt_iff hp, ← div_lt_div_right_of_neg hs']
-    -- Porting note: previously we could write `zero_lt_one` inline,
-    -- but now Lean doesn't guess we are talking about `1` fast enough.
-    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
-    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1
-    · field_simp
-    · field_simp
-    · nlinarith
-  · rw [← div_lt_iff hp, ← div_lt_div_right hs']
-    -- Porting note: previously we could write `zero_lt_one` inline,
-    -- but now Lean doesn't guess we are talking about `1` fast enough.
-    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
-    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1
-    · field_simp
-    · field_simp
-    · nlinarith
+  · rw [← div_lt_iff hp', ← div_lt_div_right_of_neg hs']
+    convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
+    · rw [add_sub_cancel_left, log_one, sub_zero]
+    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
+    · apply add_lt_add_left (mul_lt_of_one_lt_left hs' hp)
+  · rw [← div_lt_iff hp', ← div_lt_div_right hs']
+    convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
+    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
+    · rw [add_sub_cancel_left, log_one, sub_zero]
+    · apply add_lt_add_left (lt_mul_of_one_lt_left hs' hp)
 #align one_add_mul_self_lt_rpow_one_add one_add_mul_self_lt_rpow_one_add
 
 /-- **Bernoulli's inequality** for real exponents, non-strict version: for `1 ≤ p` and `-1 ≤ s`
@@ -149,28 +143,29 @@ with `s ≠ 0`, we have `(1 + s) ^ p < 1 + p * s`. -/
 theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p)
     (hp2 : p < 1) : (1 + s) ^ p < 1 + p * s := by
   rcases eq_or_lt_of_le hs with (rfl | hs)
-  · have : p ≠ 0 := by positivity
-    simpa [zero_rpow this]
-  have hs1 : 0 < 1 + s := by linarith
-  rcases le_or_lt (1 + p * s) 0 with hs2 | hs2
-  · nlinarith
+  · rwa [add_right_neg, zero_rpow hp1.ne', mul_neg, mul_one, lt_add_neg_iff_add_lt, zero_add]
+  have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
+  have hs2 : 0 < 1 + p * s := by
+    rw [← neg_lt_iff_pos_add']
+    rcases lt_or_gt_of_ne hs' with h | h
+    · exact hs.trans (lt_mul_of_lt_one_left h hp2)
+    · exact neg_one_lt_zero.trans (mul_pos hp1 h)
+  have hs3 : 1 + s ≠ 1 := hs' ∘ add_right_eq_self.mp
+  have hs4 : 1 + p * s ≠ 1 := by
+    contrapose! hs'; rwa [add_right_eq_self, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs'
   rw [rpow_def_of_pos hs1, ← exp_log hs2]
   apply exp_strictMono
-  have hs3 : 1 + s ≠ 1 := by contrapose! hs'; linarith
-  have hs4 : 1 + p * s ≠ 1 := by contrapose! hs'; nlinarith
   cases' lt_or_gt_of_ne hs' with hs' hs'
   · rw [← lt_div_iff hp1, ← div_lt_div_right_of_neg hs']
-    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
-    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs1 hs2 hs3 hs4 _ using 1
-    · field_simp
-    · field_simp
-    · nlinarith
+    convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
+    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
+    · rw [add_sub_cancel_left, log_one, sub_zero]
+    · apply add_lt_add_left (lt_mul_of_lt_one_left hs' hp2)
   · rw [← lt_div_iff hp1, ← div_lt_div_right hs']
-    haveI : (1 : ℝ) ∈ Ioi 0 := zero_lt_one
-    convert strictConcaveOn_log_Ioi.secant_strict_mono this hs2 hs1 hs4 hs3 _ using 1
-    · field_simp
-    · field_simp
-    · nlinarith
+    convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
+    · rw [add_sub_cancel_left, log_one, sub_zero]
+    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
+    · apply add_lt_add_left (mul_lt_of_lt_one_left hs' hp2)
 
 /-- **Bernoulli's inequality** for real exponents, non-strict version: for `0 ≤ p ≤ 1` and `-1 ≤ s`
 we have `(1 + s) ^ p ≤ 1 + p * s`. -/
@@ -188,48 +183,31 @@ theorem rpow_one_add_le_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp
 
 We give an elementary proof rather than using the second derivative test, since this lemma is
 needed early in the analysis library. -/
-theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   apply strictConvexOn_of_slope_strict_mono_adjacent (convex_Ici (0 : ℝ))
   rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
-  have hy : 0 < y := by linarith
+  have hy : 0 < y := hx.trans_lt hxy
   have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
-  have H1 : y ^ (p - 1 + 1) = y ^ (p - 1) * y := rpow_add_one hy.ne' _
-  ring_nf at H1
   trans p * y ^ (p - 1)
-  · have h3 : 0 < y - x := by linarith only [hxy]
-    have hyx'' : x / y < 1 := by rwa [div_lt_one hy]
-    have hyx''' : x / y - 1 < 0 := by linarith only [hyx'']
-    have hyx'''' : 0 ≤ x / y := by positivity
-    have hyx''''' : -1 ≤ x / y - 1 := by linarith only [hyx'''']
-    have : 1 - (1 + (x / y - 1)) ^ p < -p * (x / y - 1) := by
-      linarith [one_add_mul_self_lt_rpow_one_add hyx''''' hyx'''.ne hp]
-    rw [div_lt_iff h3, ← div_lt_div_right hy']
-    convert this using 1
-    · have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _
-      ring_nf at H ⊢
-      field_simp at H ⊢
-      linear_combination H
-    · ring_nf at H1 ⊢
-      field_simp
-      linear_combination p * (-y + x) * H1
-  · have hyz' : 0 < z - y := by linarith only [hyz]
-    have hyz'' : 1 < z / y := by rwa [one_lt_div hy]
-    have hyz''' : 0 < z / y - 1 := by linarith only [hyz'']
-    have hyz'''' : -1 ≤ z / y - 1 := by linarith only [hyz'']
-    have : p * (z / y - 1) < (1 + (z / y - 1)) ^ p - 1 := by
-      linarith [one_add_mul_self_lt_rpow_one_add hyz'''' hyz'''.ne' hp]
-    rw [lt_div_iff hyz', ← div_lt_div_right hy']
-    convert this using 1
-    · ring_nf at H1 ⊢
-      field_simp at H1 ⊢
-      linear_combination p * (y - z) * y ^ p * H1
-    · have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _
-      ring_nf at H ⊢
-      field_simp at H ⊢
-      linear_combination -H
+  · have q : 0 < y - x := by rwa [sub_pos]
+    rw [div_lt_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hx hy.le,
+      sub_lt_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, ← div_mul_eq_mul_div,
+      mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul,
+      sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne']
+    apply one_add_mul_self_lt_rpow_one_add _ _ hp
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hx, hy.le⟩
+    · rw [sub_ne_zero]; exact ((div_lt_one hy).mpr hxy).ne
+  · have q : 0 < z - y := by rwa [sub_pos]
+    rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le,
+      lt_tsub_iff_left, ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
+      ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
+      mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
+    apply one_add_mul_self_lt_rpow_one_add _ _ hp
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hz, hy.le⟩
+    · rw [sub_ne_zero]; exact ((one_lt_div hy).mpr hyz).ne'
 #align strict_convex_on_rpow strictConvexOn_rpow
 
-theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   rcases eq_or_lt_of_le hp with (rfl | hp)
   · simpa using convexOn_id (convex_Ici _)
   exact (strictConvexOn_rpow hp).convexOn
@@ -240,48 +218,31 @@ theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : 
 We give an elementary proof rather than using the second derivative test, since this lemma is
 needed early in the analysis library. -/
 theorem strictConcaveOn_rpow {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
-    StrictConcaveOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+    StrictConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ici (0 : ℝ))
   rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
   have hy : 0 < y := by linarith
   have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
-  have H1 : y ^ (p - 1 + 1) = y ^ (p - 1) * y := rpow_add_one hy.ne' _
-  ring_nf at H1
   trans p * y ^ (p - 1)
-  · have hyz' : 0 < z - y := by linarith only [hyz]
-    have hyz'' : 1 < z / y := by rwa [one_lt_div hy]
-    have hyz''' : 0 < z / y - 1 := by linarith only [hyz'']
-    have hyz'''' : -1 ≤ z / y - 1 := by linarith only [hyz'']
-    have : (1 + (z / y - 1)) ^ p - 1 < p * (z / y - 1) := by
-      linarith [rpow_one_add_lt_one_add_mul_self hyz'''' hyz'''.ne' hp1 hp2]
-    rw [div_lt_iff hyz', ← div_lt_div_right hy']
-    convert this using 1
-    · have H : (z / y) ^ p = z ^ p / y ^ p := div_rpow hz hy.le _
-      ring_nf at H ⊢
-      field_simp at H ⊢
-      linear_combination -H
-    · ring_nf at H1 ⊢
-      field_simp at H1 ⊢
-      linear_combination p * (y - z) * y ^ p * H1
-  · have h3 : 0 < y - x := by linarith only [hxy]
-    have hyx'' : x / y < 1 := by rwa [div_lt_one hy]
-    have hyx''' : x / y - 1 < 0 := by linarith only [hyx'']
-    have hyx'''' : 0 ≤ x / y := by positivity
-    have hyx''''' : -1 ≤ x / y - 1 := by linarith only [hyx'''']
-    have : -p * (x / y - 1) < 1 - (1 + (x / y - 1)) ^ p := by
-      linarith [rpow_one_add_lt_one_add_mul_self hyx''''' hyx'''.ne hp1 hp2]
-    rw [lt_div_iff h3, ← div_lt_div_right hy']
-    convert this using 1
-    · ring_nf at H1 ⊢
-      field_simp
-      linear_combination p * (-y + x) * H1
-    · have H : (x / y) ^ p = x ^ p / y ^ p := div_rpow hx hy.le _
-      ring_nf at H ⊢
-      field_simp at H ⊢
-      linear_combination H
+  · have q : 0 < z - y := by linarith only [hyz]
+    rw [div_lt_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le,
+      sub_lt_iff_lt_add', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
+      ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
+      mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
+    apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hz, hy.le⟩
+    · rw [sub_ne_zero]; exact ((one_lt_div hy).mpr hyz).ne'
+  · have q : 0 < y - x := by linarith only [hxy]
+    rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hx hy.le,
+      lt_sub_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, ← div_mul_eq_mul_div,
+      mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul,
+      sub_eq_add_neg 1, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne']
+    apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hx, hy.le⟩
+    · rw [sub_ne_zero]; exact ((div_lt_one hy).mpr hxy).ne
 
 theorem concaveOn_rpow {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
-    ConcaveOn ℝ (Ici 0) fun x : ℝ => x ^ p := by
+    ConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   rcases eq_or_lt_of_le hp1 with (rfl | hp1)
   · simpa using concaveOn_const (c := 1) (convex_Ici _)
   rcases eq_or_lt_of_le hp2 with (rfl | hp2)

From 5901374a8c034c74a1af273ca9c9615b1edabc12 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Sun, 24 Mar 2024 13:17:10 +0800
Subject: [PATCH 3/5] 9 yards (or 9 metres)

---
 Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 3957593f0dff4..6895cef42b3f3 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -199,7 +199,7 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0)
     · rw [sub_ne_zero]; exact ((div_lt_one hy).mpr hxy).ne
   · have q : 0 < z - y := by rwa [sub_pos]
     rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le,
-      lt_tsub_iff_left, ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
+      lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
       ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
       mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
     apply one_add_mul_self_lt_rpow_one_add _ _ hp

From 244e69b7068ad9f32976a0d49f24919027ddc3da Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Mon, 25 Mar 2024 01:06:48 +0800
Subject: [PATCH 4/5] fix all

---
 .../Convex/SpecificFunctions/Basic.lean       | 62 +++++++++----------
 1 file changed, 29 insertions(+), 33 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 6895cef42b3f3..2b20fa8bcc514 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -29,15 +29,12 @@ theory.
 
 ## See also
 
-`Analysis.Convex.Mul` for convexity of `x ↦ x ^ n``
+`Analysis.Convex.Mul` for convexity of `x ↦ x ^ n`
 -/
 
 open Real Set BigOperators NNReal
 
-/-- `Real.exp` is strictly convex on the whole real line.
-
-We give an elementary proof rather than using the second derivative test, since this lemma is
-needed early in the analysis library. -/
+/-- `Real.exp` is strictly convex on the whole real line. -/
 theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp := by
   apply strictConvexOn_of_slope_strict_mono_adjacent convex_univ
   rintro x y z - - hxy hyz
@@ -65,13 +62,10 @@ theorem convexOn_exp : ConvexOn ℝ univ exp :=
   strictConvexOn_exp.convexOn
 #align convex_on_exp convexOn_exp
 
-/- `Real.log` is strictly concave on $(0, +∞)$.
-
-We give an elementary proof rather than using the second derivative test, since this lemma is
-needed early in the analysis library. -/
+/- `Real.log` is strictly concave on $(0, +∞)$. -/
 theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
   apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
-  rintro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
+  intro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
   have hy : 0 < y := hx.trans hxy
   trans y⁻¹
   · have h : 0 < z - y := by linarith
@@ -104,8 +98,8 @@ theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log := by
 theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp : 1 < p) :
     1 + p * s < (1 + s) ^ p := by
   have hp' : 0 < p := zero_lt_one.trans hp
-  rcases eq_or_lt_of_le hs with (rfl | hs)
-  · rwa [add_right_neg, zero_rpow hp'.ne', mul_neg, mul_one, add_neg_lt_iff_lt_add, zero_add]
+  rcases eq_or_lt_of_le hs with rfl | hs
+  · rwa [add_right_neg, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
   have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
   rcases le_or_lt (1 + p * s) 0 with hs2 | hs2
   · exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
@@ -142,8 +136,8 @@ theorem one_add_mul_self_le_rpow_one_add {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp
 with `s ≠ 0`, we have `(1 + s) ^ p < 1 + p * s`. -/
 theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p)
     (hp2 : p < 1) : (1 + s) ^ p < 1 + p * s := by
-  rcases eq_or_lt_of_le hs with (rfl | hs)
-  · rwa [add_right_neg, zero_rpow hp1.ne', mul_neg, mul_one, lt_add_neg_iff_add_lt, zero_add]
+  rcases eq_or_lt_of_le hs with rfl | hs
+  · rwa [add_right_neg, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
   have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
   have hs2 : 0 < 1 + p * s := by
     rw [← neg_lt_iff_pos_add']
@@ -179,13 +173,10 @@ theorem rpow_one_add_le_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp
   · simp [hs']
   exact (rpow_one_add_lt_one_add_mul_self hs hs' hp1 hp2).le
 
-/-- For `p : ℝ` with `1 < p`, `fun x ↦ x ^ p` is strictly convex on $[0, +∞)$.
-
-We give an elementary proof rather than using the second derivative test, since this lemma is
-needed early in the analysis library. -/
+/-- For `p : ℝ` with `1 < p`, `fun x ↦ x ^ p` is strictly convex on $[0, +∞)$. -/
 theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   apply strictConvexOn_of_slope_strict_mono_adjacent (convex_Ici (0 : ℝ))
-  rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
+  intro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
   have hy : 0 < y := hx.trans_lt hxy
   have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
   trans p * y ^ (p - 1)
@@ -195,16 +186,20 @@ theorem strictConvexOn_rpow {p : ℝ} (hp : 1 < p) : StrictConvexOn ℝ (Ici 0)
       mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul,
       sub_eq_add_neg, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne']
     apply one_add_mul_self_lt_rpow_one_add _ _ hp
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hx, hy.le⟩
-    · rw [sub_ne_zero]; exact ((div_lt_one hy).mpr hxy).ne
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
+      exact Or.inl ⟨hx, hy.le⟩
+    · rw [sub_ne_zero]
+      exact ((div_lt_one hy).mpr hxy).ne
   · have q : 0 < z - y := by rwa [sub_pos]
     rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le,
       lt_sub_iff_add_lt', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
       ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
       mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
     apply one_add_mul_self_lt_rpow_one_add _ _ hp
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hz, hy.le⟩
-    · rw [sub_ne_zero]; exact ((one_lt_div hy).mpr hyz).ne'
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
+      exact Or.inl ⟨hz, hy.le⟩
+    · rw [sub_ne_zero]
+      exact ((one_lt_div hy).mpr hyz).ne'
 #align strict_convex_on_rpow strictConvexOn_rpow
 
 theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
@@ -213,14 +208,11 @@ theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : 
   exact (strictConvexOn_rpow hp).convexOn
 #align convex_on_rpow convexOn_rpow
 
-/-- For `p : ℝ` with `0 < p < 1`, `fun x ↦ x ^ p` is strictly concave on $[0, +∞)$.
-
-We give an elementary proof rather than using the second derivative test, since this lemma is
-needed early in the analysis library. -/
+/-- For `p : ℝ` with `0 < p < 1`, `fun x ↦ x ^ p` is strictly concave on $[0, +∞)$. -/
 theorem strictConcaveOn_rpow {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
     StrictConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
   apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ici (0 : ℝ))
-  rintro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
+  intro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
   have hy : 0 < y := by linarith
   have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
   trans p * y ^ (p - 1)
@@ -230,16 +222,20 @@ theorem strictConcaveOn_rpow {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
       ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
       mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
     apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hz, hy.le⟩
-    · rw [sub_ne_zero]; exact ((one_lt_div hy).mpr hyz).ne'
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
+      exact Or.inl ⟨hz, hy.le⟩
+    · rw [sub_ne_zero]
+      exact ((one_lt_div hy).mpr hyz).ne'
   · have q : 0 < y - x := by linarith only [hxy]
     rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hx hy.le,
       lt_sub_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, ← div_mul_eq_mul_div,
       mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul,
       sub_eq_add_neg 1, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne']
     apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]; exact Or.inl ⟨hx, hy.le⟩
-    · rw [sub_ne_zero]; exact ((div_lt_one hy).mpr hxy).ne
+    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
+      exact Or.inl ⟨hx, hy.le⟩
+    · rw [sub_ne_zero]
+      exact ((div_lt_one hy).mpr hxy).ne
 
 theorem concaveOn_rpow {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
     ConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
@@ -251,7 +247,7 @@ theorem concaveOn_rpow {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
 
 theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by
   refine' ⟨convex_Iio _, _⟩
-  rintro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
+  intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
   have hx' : 0 < -x := by linarith
   have hy' : 0 < -y := by linarith
   have hxy' : -x ≠ -y := by contrapose! hxy; linarith

From b5836b98ea35e3844b2b68434d9090168e9cf3d0 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Mon, 25 Mar 2024 21:14:21 +0800
Subject: [PATCH 5/5] ack

---
 .../Convex/SpecificFunctions/Basic.lean       | 42 ++--------------
 .../Convex/SpecificFunctions/Pow.lean         | 50 +++++++------------
 2 files changed, 22 insertions(+), 70 deletions(-)

diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 2b20fa8bcc514..4eea1bf2959a5 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -19,14 +19,15 @@ In this file we prove that the following functions are convex or strictly convex
   $(0, +∞)$ and $(-∞, 0)$ respectively.
 * `convexOn_rpow`, `strictConvexOn_rpow` : For `p : ℝ`, `fun x ↦ x ^ p` is convex on $[0, +∞)$ when
   `1 ≤ p` and strictly convex when `1 < p`.
-* `concaveOn_rpow`, `strictConcaveOn_rpow` : For `p : ℝ`, `fun x ↦ x ^ p` is concave on $[0, +∞)$
-  when `0 ≤ p ≤ 1` and strictly concave when `0 < p < 1`.
 
 The proofs in this file are deliberately elementary, *not* by appealing to the sign of the second
 derivative. This is in order to keep this file early in the import hierarchy, since it is on the
 path to Hölder's and Minkowski's inequalities and after that to Lp spaces and most of measure
 theory.
 
+(Strict) concavity of `fun x ↦ x ^ p` for `0 < p < 1` (`0 ≤ p ≤ 1`) can be found in
+`Analysis.Convex.SpecificFunctions.Pow`.
+
 ## See also
 
 `Analysis.Convex.Mul` for convexity of `x ↦ x ^ n`
@@ -208,43 +209,6 @@ theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : 
   exact (strictConvexOn_rpow hp).convexOn
 #align convex_on_rpow convexOn_rpow
 
-/-- For `p : ℝ` with `0 < p < 1`, `fun x ↦ x ^ p` is strictly concave on $[0, +∞)$. -/
-theorem strictConcaveOn_rpow {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
-    StrictConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
-  apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ici (0 : ℝ))
-  intro x y z (hx : 0 ≤ x) (hz : 0 ≤ z) hxy hyz
-  have hy : 0 < y := by linarith
-  have hy' : 0 < y ^ p := rpow_pos_of_pos hy _
-  trans p * y ^ (p - 1)
-  · have q : 0 < z - y := by linarith only [hyz]
-    rw [div_lt_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hz hy.le,
-      sub_lt_iff_lt_add', ← add_sub_cancel_right (z / y) 1, add_comm _ 1, add_sub_assoc,
-      ← div_mul_eq_mul_div, mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one,
-      mul_assoc, ← div_eq_inv_mul, _root_.sub_div, div_self hy.ne']
-    apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
-      exact Or.inl ⟨hz, hy.le⟩
-    · rw [sub_ne_zero]
-      exact ((one_lt_div hy).mpr hyz).ne'
-  · have q : 0 < y - x := by linarith only [hxy]
-    rw [lt_div_iff q, ← div_lt_div_right hy', _root_.sub_div, div_self hy'.ne', ← div_rpow hx hy.le,
-      lt_sub_comm, ← add_sub_cancel_right (x / y) 1, add_comm, add_sub_assoc, ← div_mul_eq_mul_div,
-      mul_div_assoc, ← rpow_sub hy, sub_sub_cancel_left, rpow_neg_one, mul_assoc, ← div_eq_inv_mul,
-      sub_eq_add_neg 1, ← mul_neg, ← neg_div, neg_sub, _root_.sub_div, div_self hy.ne']
-    apply rpow_one_add_lt_one_add_mul_self _ _ hp1 hp2
-    · rw [le_sub_iff_add_le, add_left_neg, div_nonneg_iff]
-      exact Or.inl ⟨hx, hy.le⟩
-    · rw [sub_ne_zero]
-      exact ((div_lt_one hy).mpr hxy).ne
-
-theorem concaveOn_rpow {p : ℝ} (hp1 : 0 ≤ p) (hp2 : p ≤ 1) :
-    ConcaveOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p := by
-  rcases eq_or_lt_of_le hp1 with (rfl | hp1)
-  · simpa using concaveOn_const (c := 1) (convex_Ici _)
-  rcases eq_or_lt_of_le hp2 with (rfl | hp2)
-  · simpa using concaveOn_id (convex_Ici _)
-  exact (strictConcaveOn_rpow hp1 hp2).concaveOn
-
 theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by
   refine' ⟨convex_Iio _, _⟩
   intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab
diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
index 264e8e6c5d1a5..0f01f9cc1e88f 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Pow.lean
@@ -33,32 +33,27 @@ namespace NNReal
 
 lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) :
     StrictConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p := by
-  have hp₀' : 0 < 1 / p := by positivity
+  have hp₀' : 0 < 1 / p := div_pos zero_lt_one hp₀
   have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
   let f := NNReal.orderIsoRpow (1 / p) hp₀'
   have h₁ : StrictConvexOn ℝ≥0 univ f := by
     refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-    exact (strictConvexOn_rpow hp₁').2 (by positivity : 0 ≤ x) (by positivity : 0 ≤ y)
-      (by simp [hxy]) ha hb (by simp; norm_cast)
+    exact (strictConvexOn_rpow hp₁').2 x.2 y.2 (by simp [hxy]) ha hb (by simp; norm_cast)
   have h₂ : ∀ x, f.symm x = x ^ p := by simp [f, NNReal.orderIsoRpow_symm_eq]
-  refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
+  refine ⟨convex_univ, fun x mx y my hxy a b ha hb hab => ?_⟩
   simp only [← h₂]
-  exact (f.strictConcaveOn_symm h₁).2 (Set.mem_univ x) (Set.mem_univ y) hxy ha hb hab
+  exact (f.strictConcaveOn_symm h₁).2 mx my hxy ha hb hab
 
 lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
     ConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p := by
-  if hp : p = 0 then
-    exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
-  else
-    push_neg at hp
-    if hp' : p = 1 then
-      exact ⟨convex_univ, by simp [hp']⟩
-    else
-      push_neg at hp'
-      exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
+  rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
+  · simpa only [rpow_zero] using concaveOn_const (c := 1) convex_univ
+  rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
+  · simpa only [rpow_one] using concaveOn_id convex_univ
+  exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn
 
 lemma strictConcaveOn_sqrt : StrictConcaveOn ℝ≥0 univ NNReal.sqrt := by
-  have : NNReal.sqrt = fun (x:ℝ≥0) ↦ x ^ (1 / (2:ℝ)) := by
+  have : NNReal.sqrt = fun x : ℝ≥0 ↦ x ^ (1 / (2 : ℝ)) := by
     ext x; exact mod_cast NNReal.sqrt_eq_rpow x
   rw [this]
   exact strictConcaveOn_rpow (by positivity) (by linarith)
@@ -74,30 +69,23 @@ lemma strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) :
   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
+  let a' : ℝ≥0 := ⟨a, ha.le⟩
+  let b' : ℝ≥0 := ⟨b, hb.le⟩
   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')
+  exact_mod_cast (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y')
     hxy' (mod_cast ha) (mod_cast hb) hab'
 
 lemma concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) :
     ConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p := by
-  if hp : p = 0 then
-    exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
-  else
-    push_neg at hp
-    if hp' : p = 1 then
-      exact ⟨convex_Ici 0, by simp [hp']⟩
-    else
-      push_neg at hp'
-      exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
+  rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
+  · simpa only [rpow_zero] using concaveOn_const (c := 1) (convex_Ici _)
+  rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
+  · simpa only [rpow_one] using concaveOn_id (convex_Ici _)
+  exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn
 
 lemma strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) Real.sqrt := by
-  have : Real.sqrt = fun (x:ℝ) ↦ x ^ (1 / (2:ℝ)) := by
+  have : Real.sqrt = fun x : ℝ ↦ x ^ (1 / (2 : ℝ)) := by
     ext x; exact Real.sqrt_eq_rpow x
   rw [this]
   exact strictConcaveOn_rpow (by positivity) (by linarith)