[Merged by Bors] - feat: lemmas about monotonicity and asymptotics of rpow

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -51,6 +51,72 @@ theorem tendsto_rpow_neg_atTop {y : ℝ} (hy : 0 < y) : Tendsto (fun x : ℝ =>
     (tendsto_rpow_atTop hy).inv_tendsto_atTop
 #align tendsto_rpow_neg_at_top tendsto_rpow_neg_atTop
 
+open Asymptotics in
+lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b < 1) :
+    Tendsto (rpow b) atTop (𝓝 (0:ℝ)) := by
+  show Tendsto (fun z => b^z) atTop (𝓝 0)
+  rcases lt_trichotomy b 0 with hb|rfl|hb
+  case inl =>   -- b < 0
+    simp_rw [Real.rpow_def_of_nonpos hb.le]
+    simp only [hb.ne, ite_false]
+    rw [←isLittleO_const_iff (c := (1:ℝ)) one_ne_zero]
+    have H : (1:ℝ) = 1 * 1 := by simp
+    rw [H]
+    refine IsLittleO.mul_isBigO ?exp ?cos
+    case exp =>
+      rw [isLittleO_const_iff one_ne_zero]
+      have h₀ : log b = log (- -b) := by simp
+      rw [h₀, log_neg_eq_log]
+      have hb' : 0 < -b := by linarith
+      have h₁ : log (-b) < 0 := by rw [log_neg_iff hb']; linarith
+      refine tendsto_exp_atBot.comp ?_
+      rw [tendsto_const_mul_atBot_of_neg h₁]
+      show atTop ≤ atTop
+      rfl
+    case cos =>
+      rw [isBigO_iff]
+      exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
+  case inr.inl =>  -- b = 0
+    simp only [log_zero, zero_mul, exp_zero, one_mul, ite_true]
+    refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
+    rw [tendsto_pure]
+    filter_upwards [eventually_ne_atTop 0] with _ hx
+    simp [hx]
+  case inr.inr =>   -- b > 0
+    simp_rw [Real.rpow_def_of_pos hb]
+    have h₁ : log b < 0 := by rw [log_neg_iff hb]; exact hb₁
+    refine tendsto_exp_atBot.comp ?_
+    rw [tendsto_const_mul_atBot_of_neg h₁]
+    show atTop ≤ atTop
+    rfl
+
+lemma tendsto_rpow_atTop_of_base_gt_one (b : ℝ) (hb : 1 < b) :
+    Tendsto (rpow b) atBot (𝓝 (0:ℝ)) := by
+  show Tendsto (fun z => b^z) atBot (nhds 0)
+  simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
+  refine tendsto_exp_atBot.comp ?_
+  have h₁ : 0 < log b := by rw [log_pos_iff (by positivity)]; aesop
+  rw [tendsto_const_mul_atBot_of_pos h₁]
+  exact tendsto_id
+
+lemma tendsto_rpow_atBot_of_base_lt_one (b : ℝ) (hb₀ : 0 < b) (hb₁ : b < 1) :
+    Tendsto (rpow b) atBot atTop := by
+  show Tendsto (fun z => b^z) atBot atTop
+  simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
+  refine tendsto_exp_atTop.comp ?_
+  have h₁ : log b < 0 := by rw [log_neg_iff hb₀]; exact hb₁
+  rw [tendsto_const_mul_atTop_iff_neg (by show atBot ≤ atBot; simp)]
+  exact h₁
+
+lemma tendsto_rpow_atBot_of_base_gt_one (b : ℝ) (hb : 1 < b) : Tendsto (rpow b) atBot (𝓝 0) := by
+  show Tendsto (fun z => b^z) atBot (𝓝 0)
+  simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]
+  refine tendsto_exp_atBot.comp ?_
+  have h₁ : 0 < log b := by rw [log_pos_iff (by positivity)]; aesop
+  rw [tendsto_const_mul_atBot_iff_pos (by show atBot ≤ atBot; simp)]
+  exact h₁
+
+
 /-- The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and
 `c` such that `b` is nonzero. -/
 theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) :

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -477,6 +477,24 @@ theorem rpow_le_rpow_of_exponent_le (hx : 1 ≤ x) (hyz : y ≤ z) : x ^ y ≤ x
   rw [exp_le_exp]; exact mul_le_mul_of_nonneg_left hyz (log_nonneg hx)
 #align real.rpow_le_rpow_of_exponent_le Real.rpow_le_rpow_of_exponent_le
 
+theorem rpow_lt_rpow_of_exponent_neg {x y z : ℝ} (hy : 0 < y) (hxy : y < x) (hz : z < 0) :
+    x ^ z < y ^ z := by
+  have hx : 0 < x := hy.trans hxy
+  rw [←neg_neg z, Real.rpow_neg (le_of_lt hx) (-z), Real.rpow_neg (le_of_lt hy) (-z),
+      inv_lt_inv (rpow_pos_of_pos hx _) (rpow_pos_of_pos hy _)]
+  exact Real.rpow_lt_rpow (by positivity) hxy <| neg_pos_of_neg hz
+
+theorem rpow_le_rpow_of_exponent_nonpos {x y : ℝ} (hy : 0 < y) (hxy : y ≤ x) (hz : z ≤ 0) :
+    x ^ z ≤ y ^ z := by
+  rcases ne_or_eq z 0 with hz_zero | rfl
+  case inl =>
+    rcases ne_or_eq x y with hxy' | rfl
+    case inl =>
+      exact le_of_lt <| rpow_lt_rpow_of_exponent_neg hy (Ne.lt_of_le (id (Ne.symm hxy')) hxy)
+        (Ne.lt_of_le hz_zero hz)
+    case inr => simp
+  case inr => simp
+
 @[simp]
 theorem rpow_le_rpow_left_iff (hx : 1 < x) : x ^ y ≤ x ^ z ↔ y ≤ z := by
   have x_pos : 0 < x := lt_trans zero_lt_one hx
@@ -634,6 +652,31 @@ theorem rpow_nat_inv_pow_nat {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) :
   rw [← rpow_nat_cast, ← rpow_mul hx, inv_mul_cancel hn0, rpow_one]
 #align real.rpow_nat_inv_pow_nat Real.rpow_nat_inv_pow_nat
 
+lemma strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) :
+    StrictMono (rpow b) := by
+  show StrictMono (fun (x:ℝ) => b ^ x)
+  simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
+  exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb
+
+lemma monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) :
+    Monotone (rpow b) := by
+  rcases lt_or_eq_of_le hb with hb | rfl
+  case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
+  case inr => intro _ _ _; simp
+
+lemma strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) :
+    StrictAnti (rpow b) := by
+  show StrictAnti (fun (x:ℝ) => b ^ x)
+  simp_rw [Real.rpow_def_of_pos hb₀]
+  exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
+      <| Real.log_neg hb₀ hb₁
+
+lemma antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) :
+    Antitone (rpow b) := by
+  rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
+  case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
+  case inr => intro _ _ _; simp
+
 end Real
 
 /-!