feat: Bernoulli's inequality for 0 < p < 1 (#10982)

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

Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

@@ -21,26 +21,21 @@ In this file we prove that the following functions are convex or strictly convex
   `1 ≤ p` and strictly convex when `1 < p`.
 
 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`.
+(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``
+`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
@@ -68,13 +63,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
@@ -106,34 +98,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
-  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
+  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_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`
@@ -147,60 +133,85 @@ 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
+  · 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']
+    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
+  cases' lt_or_gt_of_ne hs' with hs' hs'
+  · rw [← lt_div_iff hp1, ← div_lt_div_right_of_neg 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_lt_one_left hs' hp2)
+  · rw [← lt_div_iff hp1, ← div_lt_div_right 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_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`. -/
+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
 
-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
+/-- 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
-  have hy : 0 < y := by linarith
+  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 _
-  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_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'
 #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
 #align convex_on_rpow convexOn_rpow
 
 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
@@ -209,7 +220,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

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)