chore: forward-port #19026 (#4129)

Fiddly, not done yet ... help welcome.

Cross-reference: leanprover-community/mathlib3#19026.



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: 4 people

Mathlib/Analysis/Convex/Slope.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudriashov, Malo Jaffré
 
 ! This file was ported from Lean 3 source module analysis.convex.slope
-! leanprover-community/mathlib commit 78261225eb5cedc61c5c74ecb44e5b385d13b733
+! leanprover-community/mathlib commit a8b2226cfb0a79f5986492053fc49b1a0c6aeffb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -237,6 +237,114 @@ theorem strictConcaveOn_iff_slope_strict_anti_adjacent :
     strictConcaveOn_of_slope_strict_anti_adjacent h.1 (@fun _ _ _ hx hy => h.2 hx hy)⟩
 #align strict_concave_on_iff_slope_strict_anti_adjacent strictConcaveOn_iff_slope_strict_anti_adjacent
 
+theorem ConvexOn.secant_mono_aux1 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
+    (hxy : x < y) (hyz : y < z) : (z - x) * f y ≤ (z - y) * f x + (y - x) * f z := by
+  have hxy' : 0 < y - x := by linarith
+  have hyz' : 0 < z - y := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [← le_div_iff' hxz']
+  have ha : 0 ≤ (z - y) / (z - x) := by positivity
+  have hb : 0 ≤ (y - x) / (z - x) := by positivity
+  calc
+    f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) := ?_
+    _ ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := hf.2 hx hz ha hb ?_
+    _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
+  · congr 1
+    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    ring
+  · -- Porting note: this `show` wasn't needed in Lean 3
+    show (z - y) / (z - x) + (y - x) / (z - x) = 1
+    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+  · field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+#align convex_on.secant_mono_aux1 ConvexOn.secant_mono_aux1
+
+theorem ConvexOn.secant_mono_aux2 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
+    (hxy : x < y) (hyz : y < z) : (f y - f x) / (y - x) ≤ (f z - f x) / (z - x) := by
+  have hxy' : 0 < y - x := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [div_le_div_iff hxy' hxz']
+  linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
+#align convex_on.secant_mono_aux2 ConvexOn.secant_mono_aux2
+
+theorem ConvexOn.secant_mono_aux3 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
+    (hxy : x < y) (hyz : y < z) : (f z - f x) / (z - x) ≤ (f z - f y) / (z - y) := by
+  have hyz' : 0 < z - y := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [div_le_div_iff hxz' hyz']
+  linarith only [hf.secant_mono_aux1 hx hz hxy hyz]
+#align convex_on.secant_mono_aux3 ConvexOn.secant_mono_aux3
+
+theorem ConvexOn.secant_mono (hf : ConvexOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s) (hx : x ∈ s)
+    (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x ≤ y) :
+    (f x - f a) / (x - a) ≤ (f y - f a) / (y - a) := by
+  rcases eq_or_lt_of_le hxy with (rfl | hxy)
+  · simp
+  cases' lt_or_gt_of_ne hxa with hxa hxa
+  · cases' lt_or_gt_of_ne hya with hya hya
+    · convert hf.secant_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> field_simp
+    · convert hf.slope_mono_adjacent hx hy hxa hya using 1
+      rw [← neg_div_neg_eq]; field_simp
+  · exact hf.secant_mono_aux2 ha hy hxa hxy
+#align convex_on.secant_mono ConvexOn.secant_mono
+
+theorem StrictConvexOn.secant_strict_mono_aux1 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
+    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (z - x) * f y < (z - y) * f x + (y - x) * f z := by
+  have hxy' : 0 < y - x := by linarith
+  have hyz' : 0 < z - y := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [← lt_div_iff' hxz']
+  have ha : 0 < (z - y) / (z - x) := by positivity
+  have hb : 0 < (y - x) / (z - x) := by positivity
+  calc
+    f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) := ?_
+    _ < (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := (hf.2 hx hz (by linarith) ha hb ?_)
+    _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_
+  · congr 1
+    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+    ring
+  · -- Porting note: this `show` wasn't needed in Lean 3
+    show (z - y) / (z - x) + (y - x) / (z - x) = 1
+    field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+  · field_simp [hxy'.ne', hyz'.ne', hxz'.ne']
+#align strict_convex_on.secant_strict_mono_aux1 StrictConvexOn.secant_strict_mono_aux1
+
+theorem StrictConvexOn.secant_strict_mono_aux2 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
+    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f y - f x) / (y - x) < (f z - f x) / (z - x) := by
+  have hxy' : 0 < y - x := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [div_lt_div_iff hxy' hxz']
+  linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
+#align strict_convex_on.secant_strict_mono_aux2 StrictConvexOn.secant_strict_mono_aux2
+
+theorem StrictConvexOn.secant_strict_mono_aux3 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
+    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f z - f x) / (z - x) < (f z - f y) / (z - y) := by
+  have hyz' : 0 < z - y := by linarith
+  have hxz' : 0 < z - x := by linarith
+  rw [div_lt_div_iff hxz' hyz']
+  linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]
+#align strict_convex_on.secant_strict_mono_aux3 StrictConvexOn.secant_strict_mono_aux3
+
+theorem StrictConvexOn.secant_strict_mono (hf : StrictConvexOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s)
+    (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x < y) :
+    (f x - f a) / (x - a) < (f y - f a) / (y - a) := by
+  cases' lt_or_gt_of_ne hxa with hxa hxa
+  · cases' lt_or_gt_of_ne hya with hya hya
+    · convert hf.secant_strict_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;>
+        field_simp
+    · convert hf.slope_strict_mono_adjacent hx hy hxa hya using 1
+      rw [← neg_div_neg_eq]; field_simp
+  · exact hf.secant_strict_mono_aux2 ha hy hxa hxy
+#align strict_convex_on.secant_strict_mono StrictConvexOn.secant_strict_mono
+
+theorem StrictConcaveOn.secant_strict_mono (hf : StrictConcaveOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s)
+    (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x < y) :
+    (f y - f a) / (y - a) < (f x - f a) / (x - a) := by
+  have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy
+  simp only [Pi.neg_apply] at key
+  rw [← neg_lt_neg_iff]
+  convert key using 1 <;> field_simp <;> ring
+#align strict_concave_on.secant_strict_mono StrictConcaveOn.secant_strict_mono
+
 /-- If `f` is convex on a set `s` in a linearly ordered field, and `f x < f y` for two points
 `x < y` in `s`, then `f` is strictly monotone on `s ∩ [y, ∞)`. -/
 theorem ConvexOn.strict_mono_of_lt (hf : ConvexOn 𝕜 s f) {x y : 𝕜} (hx : x ∈ s) (hxy : x < y)

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 
 ! This file was ported from Lean 3 source module analysis.special_functions.log.basic
-! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2
+! leanprover-community/mathlib commit a8b2226cfb0a79f5986492053fc49b1a0c6aeffb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -219,6 +219,13 @@ theorem log_injOn_pos : Set.InjOn log (Set.Ioi 0) :=
   strictMonoOn_log.injOn
 #align real.log_inj_on_pos Real.log_injOn_pos
 
+theorem log_lt_sub_one_of_pos (hx1 : 0 < x) (hx2 : x ≠ 1) : log x < x - 1 := by
+  have h : log x ≠ 0
+  · rwa [← log_one, log_injOn_pos.ne_iff hx1]
+    exact mem_Ioi.mpr zero_lt_one
+  linarith [add_one_lt_exp_of_nonzero h, exp_log hx1]
+#align real.log_lt_sub_one_of_pos Real.log_lt_sub_one_of_pos
+
 theorem eq_one_of_pos_of_log_eq_zero {x : ℝ} (h₁ : 0 < x) (h₂ : log x = 0) : x = 1 :=
   log_injOn_pos (Set.mem_Ioi.2 h₁) (Set.mem_Ioi.2 zero_lt_one) (h₂.trans Real.log_one.symm)
 #align real.eq_one_of_pos_of_log_eq_zero Real.eq_one_of_pos_of_log_eq_zero

Mathlib/Data/Complex/Exponential.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir
 
 ! This file was ported from Lean 3 source module data.complex.exponential
-! leanprover-community/mathlib commit caa58cbf5bfb7f81ccbaca4e8b8ac4bc2b39cc1c
+! leanprover-community/mathlib commit a8b2226cfb0a79f5986492053fc49b1a0c6aeffb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1472,27 +1472,36 @@ nonrec theorem sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x := by
   rw [← ofReal_inj]; simp [sinh_three_mul]
 #align real.sinh_three_mul Real.sinh_three_mul
 
-open IsAbsoluteValue
+open IsAbsoluteValue Nat
 
-/-- This is an intermediate result that is later replaced by `Real.add_one_le_exp`; use that lemma
-instead. -/
-theorem add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x :=
+theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : (∑ i in range n, x ^ i / i !) ≤ exp x :=
   calc
-    x + 1 ≤ CauSeq.lim (⟨fun n : ℕ => ((exp' x) n).re, isCauSeq_re (exp' x)⟩ : CauSeq ℝ Abs.abs) :=
-      le_lim
-        (CauSeq.le_of_exists
-          ⟨2, fun j hj =>
-            show x + (1 : ℝ) ≤ (∑ m in range j, ((x : ℂ) ^ m / m.factorial)).re by
-              have h₁ : (((fun m : ℕ => ((x : ℂ) ^ m / m.factorial)) ∘ Nat.succ) 0).re = x :=
-                by simp [show Nat.succ 0 = 1 from rfl, Complex.ofReal_re]
-              have h₂ : ((x : ℂ) ^ 0 / (Nat.factorial 0)).re = 1 := by simp
-              erw [← tsub_add_cancel_of_le hj, sum_range_succ', sum_range_succ', add_re, add_re, h₁,
-                h₂, add_assoc, ← coe_reAddGroupHom, reAddGroupHom.map_sum,
-                coe_reAddGroupHom]
-              refine' le_add_of_nonneg_of_le (sum_nonneg fun m _ => _) le_rfl
-              rw [← ofReal_pow, ← ofReal_nat_cast, ← ofReal_div, ofReal_re]
-              exact div_nonneg (pow_nonneg hx _) (Nat.cast_nonneg _)⟩)
+    (∑ i in range n, x ^ i / i !) ≤ lim (⟨_, isCauSeq_re (exp' x)⟩ : CauSeq ℝ Abs.abs) := by
+      refine' le_lim (CauSeq.le_of_exists ⟨n, fun j hj => _⟩)
+      simp only [exp', const_apply, re_sum]
+      norm_cast
+      rw [← Nat.add_sub_of_le hj, Finset.sum_range_add]
+      refine' le_add_of_nonneg_right (sum_nonneg fun i _ => _)
+      positivity
     _ = exp x := by rw [exp, Complex.exp, ← cauSeqRe, lim_re]
+#align real.sum_le_exp_of_nonneg Real.sum_le_exp_of_nonneg
+
+theorem quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2 ≤ exp x :=
+  calc
+    1 + x + x ^ 2 / 2 = ∑ i in range 3, x ^ i / i ! := by simp [Finset.sum_range_succ]; ring_nf
+    _ ≤ exp x := sum_le_exp_of_nonneg hx 3
+#align real.quadratic_le_exp_of_nonneg Real.quadratic_le_exp_of_nonneg
+
+theorem add_one_lt_exp_of_pos {x : ℝ} (hx : 0 < x) : x + 1 < exp x :=
+  (by nlinarith : x + 1 < 1 + x + x ^ 2 / 2).trans_le (quadratic_le_exp_of_nonneg hx.le)
+#align real.add_one_lt_exp_of_pos Real.add_one_lt_exp_of_pos
+
+/-- This is an intermediate result that is later replaced by `Real.add_one_le_exp`; use that lemma
+instead. -/
+theorem add_one_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : x + 1 ≤ exp x := by
+  rcases eq_or_lt_of_le hx with (rfl | h)
+  · simp
+  exact (add_one_lt_exp_of_pos h).le
 #align real.add_one_le_exp_of_nonneg Real.add_one_le_exp_of_nonneg
 
 theorem one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x := by linarith [add_one_le_exp_of_nonneg hx]
@@ -1957,67 +1966,67 @@ theorem cos_two_neg : cos 2 < 0 :=
     _ < 0 := by norm_num
 #align real.cos_two_neg Real.cos_two_neg
 
---Porting note: removed `(h1 : 0 ≤ x)` because it is no longer used
-theorem exp_bound_div_one_sub_of_interval_approx {x : ℝ} (h2 : x ≤ 1) :
-    (∑ j : ℕ in Finset.range 3, x ^ j / j.factorial) +
-        x ^ 3 * ((3 : ℕ) + 1) / ((3 : ℕ).factorial * (3 : ℕ)) ≤
-      ∑ j in Finset.range 3, x ^ j :=
+theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) :
+    Real.exp x < 1 / (1 - x) := by
+  have H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
+  · calc
+      0 < x ^ 3 := by positivity
+      _ = 1 - (1 + x + x ^ 2) * (1 - x) := by ring
   calc
-    (∑ j : ℕ in Finset.range 3, x ^ j / j.factorial) +
-        x ^ 3 * ((3 : ℕ) + 1) / ((3 : ℕ).factorial * (3 : ℕ))
-      = (2 / 9) * x ^ 3 + x ^ 2 / 2 + x + 1 := by simp [Finset.sum]; ring
-    _ ≤ x ^ 2 + x + 1 := sub_nonneg.1 <|
-      calc 0 ≤ x^2 * (2 / 9) * (9 / 4 - x) :=
-          mul_nonneg (mul_nonneg (pow_two_nonneg _) (by norm_num : (0 : ℝ) ≤ 2 / 9))
-            (sub_nonneg.2 (le_trans h2 (by norm_num)))
-        _ = _ := by ring
-    _ = _ := by simp [Finset.sum]; ring
-#align real.exp_bound_div_one_sub_of_interval_approx Real.exp_bound_div_one_sub_of_interval_approxₓ
+    exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
+    _ ≤ 1 + x + x ^ 2 := by
+      -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
+      -- This proof should be restored after the norm_num plugin for big operators is ported.
+      -- (It may also need the positivity extensions in #3907.)
+      rw [Finset.sum, range_val]
+      nth_rw 1 [← two_add_one_eq_three]
+      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
+      nth_rw 3 [← one_add_one_eq_two]
+      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
+      nth_rw 3 [← zero_add 1]
+      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
+      rw [Multiset.range_zero, Multiset.map_zero, Multiset.sum_zero]
+      norm_num
+      nlinarith
+    _ < 1 / (1 - x) := by rw [lt_div_iff] <;> nlinarith
+#align real.exp_bound_div_one_sub_of_interval' Real.exp_bound_div_one_sub_of_interval'
 
 theorem exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) :
-    Real.exp x ≤ 1 / (1 - x) :=
-  haveI h : (∑ j in Finset.range 3, x ^ j) ≤ 1 / (1 - x) := by
-    norm_num [Finset.sum]
-    have h1x : 0 < 1 - x := by simpa
-    rw [inv_eq_one_div, le_div_iff h1x]
-    norm_num [← add_assoc, mul_sub_left_distrib, mul_one, add_mul, sub_add_eq_sub_sub,
-      pow_succ' x 2]
-    have hx3 : 0 ≤ x ^ 3 := by
-      norm_num
-      simp [h1]
-    simp [Finset.sum]
-    linarith
-  (exp_bound' h1 h2.le <| by linarith).trans
-    ((exp_bound_div_one_sub_of_interval_approx h2.le).trans h)
+    Real.exp x ≤ 1 / (1 - x) := by
+  rcases eq_or_lt_of_le h1 with (rfl | h1)
+  · simp
+  · exact (exp_bound_div_one_sub_of_interval' h1 h2).le
 #align real.exp_bound_div_one_sub_of_interval Real.exp_bound_div_one_sub_of_interval
 
-theorem one_sub_le_exp_minus_of_pos {y : ℝ} (h : 0 ≤ y) : 1 - y ≤ Real.exp (-y) := by
-  rw [Real.exp_neg]
-  have r1 : (1 - y) * Real.exp y ≤ 1 := by
-    cases le_or_lt (1 - y) 0
-    · have h'' : (1 - y) * y.exp ≤ 0 := by
-        rw [mul_nonpos_iff]
-        right
-        exact ⟨by assumption, y.exp_pos.le⟩
-      linarith
-    have hy1 : y < 1 := by linarith
-    rw [← le_div_iff' ‹0 < 1 - y›]
-    exact exp_bound_div_one_sub_of_interval h hy1
-  rw [inv_eq_one_div]
-  rw [le_div_iff' y.exp_pos]
-  rwa [mul_comm] at r1
-#align real.one_sub_le_exp_minus_of_pos Real.one_sub_le_exp_minus_of_pos
-
-theorem add_one_le_exp_of_nonpos {x : ℝ} (h : x ≤ 0) : x + 1 ≤ Real.exp x := by
-  rw [add_comm]
-  have h1 : 0 ≤ -x := by linarith
-  simpa using one_sub_le_exp_minus_of_pos h1
-#align real.add_one_le_exp_of_nonpos Real.add_one_le_exp_of_nonpos
+theorem one_sub_lt_exp_minus_of_pos {y : ℝ} (h : 0 < y) : 1 - y < Real.exp (-y) := by
+  cases' le_or_lt 1 y with h' h'
+  · linarith [(-y).exp_pos]
+  rw [exp_neg, lt_inv _ y.exp_pos, inv_eq_one_div]
+  · exact exp_bound_div_one_sub_of_interval' h h'
+  · linarith
+#align real.one_sub_le_exp_minus_of_pos Real.one_sub_lt_exp_minus_of_pos
+
+theorem one_sub_le_exp_minus_of_nonneg {y : ℝ} (h : 0 ≤ y) : 1 - y ≤ Real.exp (-y) := by
+  rcases eq_or_lt_of_le h with (rfl | h)
+  · simp
+  · exact (one_sub_lt_exp_minus_of_pos h).le
+#align real.one_sub_le_exp_minus_of_nonneg Real.one_sub_le_exp_minus_of_nonneg
+
+theorem add_one_lt_exp_of_neg {x : ℝ} (h : x < 0) : x + 1 < Real.exp x := by
+  have h1 : 0 < -x := by linarith
+  simpa [add_comm] using one_sub_lt_exp_minus_of_pos h1
+#align real.add_one_lt_exp_of_neg Real.add_one_lt_exp_of_neg
+
+theorem add_one_lt_exp_of_nonzero {x : ℝ} (hx : x ≠ 0) : x + 1 < Real.exp x := by
+  cases' lt_or_gt_of_ne hx with h h
+  · exact add_one_lt_exp_of_neg h
+  exact add_one_lt_exp_of_pos h
+#align real.add_one_lt_exp_of_nonzero Real.add_one_lt_exp_of_nonzero
 
 theorem add_one_le_exp (x : ℝ) : x + 1 ≤ Real.exp x := by
   cases' le_or_lt 0 x with h h
   · exact Real.add_one_le_exp_of_nonneg h
-  exact add_one_le_exp_of_nonpos h.le
+  exact (add_one_lt_exp_of_neg h).le
 #align real.add_one_le_exp Real.add_one_le_exp
 
 theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t / n) ^ n ≤ exp (-t) := by