feat: inequalities on complex exponentials (#20844)

Two inequalities on complex exponentials:
```lean
abs (cexp x - ∑ m ∈ range n, x ^ m / m.factorial)
    ≤ Real.exp (abs x) - ∑ m ∈ range n, (abs x) ^ m / m.factorial

abs (cexp x - ∑ m ∈ range n, x ^ m / m.factorial) ≤ abs x ^ n * Real.exp (abs x)
```

Author: RemyDegenne

Mathlib/Data/Complex/Exponential.lean

@@ -1175,6 +1175,71 @@ theorem abs_exp_sub_one_sub_id_le {x : ℂ} (hx : abs x ≤ 1) : abs (exp x - 1
     _ ≤ abs x ^ 2 * 1 := by gcongr; norm_num [Nat.factorial]
     _ = abs x ^ 2 := by rw [mul_one]
 
+lemma abs_exp_sub_sum_le_exp_abs_sub_sum (x : ℂ) (n : ℕ) :
+    abs (exp x - ∑ m ∈ range n, x ^ m / m.factorial)
+      ≤ Real.exp (abs x) - ∑ m ∈ range n, (abs x) ^ m / m.factorial := by
+  rw [← CauSeq.lim_const (abv := Complex.abs) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
+    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_abs]
+  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
+  simp_rw [← sub_eq_add_neg]
+  calc abs ((∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial)
+  _ ≤ (∑ m ∈ range j, abs x ^ m / m.factorial) - ∑ m ∈ range n, abs x ^ m / m.factorial := by
+    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
+    refine (IsAbsoluteValue.abv_sum Complex.abs ..).trans_eq ?_
+    congr with i
+    simp
+  _ ≤ Real.exp (abs x) - ∑ m ∈ range n, (abs x) ^ m / m.factorial := by
+    gcongr
+    exact Real.sum_le_exp_of_nonneg (by exact AbsoluteValue.nonneg abs x) _
+
+lemma abs_exp_le_exp_abs (x : ℂ) : abs (exp x) ≤ Real.exp (abs x) := by
+  convert abs_exp_sub_sum_le_exp_abs_sub_sum x 0 using 1 <;> simp
+
+lemma abs_exp_sub_sum_le_abs_mul_exp (x : ℂ) (n : ℕ) :
+    abs (exp x - ∑ m ∈ range n, x ^ m / m.factorial) ≤ abs x ^ n * Real.exp (abs x) := by
+  rw [← CauSeq.lim_const (abv := Complex.abs) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
+    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_abs]
+  refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
+  simp_rw [← sub_eq_add_neg]
+  show abs ((∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial) ≤ _
+  rw [sum_range_sub_sum_range hj]
+  calc
+    abs (∑ m ∈ range j with n ≤ m, (x ^ m / m.factorial : ℂ))
+      = abs (∑ m ∈ range j with n ≤ m, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)) := by
+      refine congr_arg abs (sum_congr rfl fun m hm => ?_)
+      rw [mem_filter, mem_range] at hm
+      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
+    _ ≤ ∑ m ∈ range j with n ≤ m, abs (x ^ n * (x ^ (m - n) / m.factorial)) :=
+      IsAbsoluteValue.abv_sum Complex.abs ..
+    _ ≤ ∑ m ∈ range j with n ≤ m, abs x ^ n * (abs x ^ (m - n) / (m - n).factorial) := by
+      simp_rw [map_mul, map_pow, map_div₀, abs_natCast]
+      gcongr with i hi
+      · rw [IsAbsoluteValue.abv_pow abs]
+      · simp
+    _ = abs x ^ n * ∑ m ∈ range j with n ≤ m, (abs x ^ (m - n) / (m - n).factorial) := by
+      rw [← mul_sum]
+    _ = abs x ^ n * ∑ m ∈ range (j - n), (abs x ^ m / m.factorial) := by
+      congr 1
+      refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
+      · intro a ha
+        simp only [mem_filter, mem_range, le_add_iff_nonneg_left, zero_le, and_true]
+        simp only [mem_range] at ha
+        rwa [← lt_tsub_iff_right]
+      · intro a ha b hb hab
+        simpa using hab
+      · intro b hb
+        simp only [mem_range, exists_prop]
+        simp only [mem_filter, mem_range] at hb
+        refine ⟨b - n, ?_, ?_⟩
+        · rw [tsub_lt_tsub_iff_right hb.2]
+          exact hb.1
+        · rw [tsub_add_cancel_of_le hb.2]
+      · simp
+    _ ≤ abs x ^ n * Real.exp (abs x) := by
+      gcongr
+      refine Real.sum_le_exp_of_nonneg ?_ _
+      exact AbsoluteValue.nonneg abs x
+
 end Complex
 
 namespace Real