feat(data/complex/exponential): bound on exp for arbitrary arguments (#8667)

This PR is for a new lemma (currently called `exp_bound'`) which proves `exp x` is close to its `n`th degree taylor expansion for sufficiently large `n`. Unlike the previous bound, this lemma can be instantiated on any real `x` rather than just `x` with absolute value less than or equal to 1. I am separating this lemma out from #8002 because I think it stands on its own.

The last time I checked it was sorry free - but that was before I merged with master and moved it to a different branch. It may also benefit from a little golfing.

There are a few lemmas I proved as well to support this - one about the relative size of factorials and a few about sums of geometric sequences. The ~~geometric series ones should probably be generalized and moved to another file~~ this generalization sort of exists and is in the algebra.geom_sum file. I didn't find it initially since I was searching for "geometric" not "geom".

Author: BoltonBailey

src/algebra/big_operators/basic.lean

@@ -774,6 +774,12 @@ begin
   { rw [nat.add_succ, prod_range_succ, hm, prod_range_succ, mul_assoc], },
 end
 
+@[to_additive]
+lemma prod_range_add_div_prod_range {α : Type*} [comm_group α] (f : ℕ → α) (n m : ℕ) :
+  (∏ k in range (n + m), f k) / (∏ k in range n, f k) = ∏ k in finset.range m, f (n + k) :=
+div_eq_of_eq_mul' (prod_range_add f n m)
+
+
 @[to_additive]
 lemma prod_range_zero (f : ℕ → β) :
   ∏ k in range 0, f k = 1 :=

src/algebra/group/basic.lean

@@ -336,6 +336,8 @@ calc  a / 1 = a * 1⁻¹ : div_eq_mul_inv a 1
 end group
 
 section add_group
+-- TODO: Generalize the contents of this section with to_additive as per
+-- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238667
 variables {G : Type u} [add_group G] {a b c d : G}
 
 @[simp] lemma sub_self (a : G) : a - a = 0 :=
@@ -445,9 +447,15 @@ variables {G : Type u} [comm_group G]
 lemma mul_inv (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
 by rw [mul_inv_rev, mul_comm]
 
+@[to_additive]
+lemma div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c :=
+by rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
+
 end comm_group
 
 section add_comm_group
+-- TODO: Generalize the contents of this section with to_additive as per
+-- https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238667
 variables {G : Type u} [add_comm_group G] {a b c d : G}
 
 local attribute [simp] add_assoc add_comm add_left_comm sub_eq_add_neg
@@ -473,9 +481,6 @@ by simp
 lemma eq_sub_of_add_eq' (h : c + a = b) : a = b - c :=
 by simp [h.symm]
 
-lemma sub_eq_of_eq_add' (h : a = b + c) : a - b = c :=
-begin simp [h], rw [add_left_comm], simp end
-
 lemma eq_add_of_sub_eq' (h : a - b = c) : a = b + c :=
 by simp [h.symm]
 

src/data/complex/exponential.lean

@@ -210,6 +210,7 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij
     mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩,
   sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (nat.add_sub_cancel _ _).symm⟩⟩⟩)
 
+-- TODO move to src/algebra/big_operators/basic.lean, rewrite with comm_group, and make to_additive
 lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α}
   {n m : ℕ} (hnm : n ≤ m) : ∑ k in range m, f k - ∑ k in range n, f k =
   ∑ k in (range m).filter (λ k, n ≤ k), f k :=
@@ -1279,17 +1280,52 @@ begin
       refine sum_le_sum (λ m hm, _),
       rw [abs_mul, abv_pow abs, abs_div, abs_cast_nat],
       refine mul_le_mul_of_nonneg_left ((div_le_div_right _).2 _) _,
-      exact nat.cast_pos.2 (nat.factorial_pos _),
-      rw abv_pow abs,
-      exact (pow_le_one _ (abs_nonneg _) hx),
-      exact pow_nonneg (abs_nonneg _) _
+      { exact nat.cast_pos.2 (nat.factorial_pos _), },
+      { rw abv_pow abs,
+        exact (pow_le_one _ (abs_nonneg _) hx), },
+      { exact pow_nonneg (abs_nonneg _) _ },
     end
   ... = abs x ^ n * (∑ m in (range j).filter (λ k, n ≤ k), (1 / m! : ℝ)) :
     by simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm]
   ... ≤ abs x ^ n * (n.succ * (n! * n)⁻¹) :
     mul_le_mul_of_nonneg_left (sum_div_factorial_le _ _ hn) (pow_nonneg (abs_nonneg _) _)
 end
 
+lemma exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / (n.succ) ≤ 1 / 2) :
+  abs (exp x - ∑ m in range n, x ^ m / m!) ≤ abs x ^ n / (n!) * 2 :=
+begin
+  rw [← lim_const (∑ m in range n, _), exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs],
+  refine lim_le (cau_seq.le_of_exists ⟨n, λ j hj, _⟩),
+  simp_rw [←sub_eq_add_neg],
+  show abs (∑ m in range j, x ^ m / m! - ∑ m in range n, x ^ m / m!) ≤ abs x ^ n / (n!) * 2,
+  let k := j - n,
+  have hj : j = n + k := (nat.add_sub_of_le hj).symm,
+  rw [hj, sum_range_add_sub_sum_range],
+  calc abs (∑ (i : ℕ) in range k, x ^ (n + i) / ((n + i)! : ℂ))
+      ≤ ∑ (i : ℕ) in range k, abs (x ^ (n + i) / ((n + i)! : ℂ)) : abv_sum_le_sum_abv _ _
+  ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n + i)! :
+        by simp only [complex.abs_cast_nat, complex.abs_div, abv_pow abs]
+  ... ≤ ∑ (i : ℕ) in range k, (abs x) ^ (n + i) / (n! * n.succ ^ i) : _
+  ... = ∑ (i : ℕ) in range k, (abs x) ^ (n) / (n!) * ((abs x)^i / n.succ ^ i) : _
+  ... ≤ abs x ^ n / (↑n!) * 2 : _,
+  { refine sum_le_sum (λ m hm, div_le_div (pow_nonneg (abs_nonneg x) (n + m)) (le_refl _) _ _),
+    { exact_mod_cast mul_pos n.factorial_pos (pow_pos n.succ_pos _), },
+    { exact_mod_cast (nat.factorial_mul_pow_le_factorial), }, },
+  { refine finset.sum_congr rfl (λ _ _, _),
+    simp only [pow_add, div_eq_inv_mul, mul_inv', mul_left_comm, mul_assoc], },
+  { rw [←mul_sum],
+    apply mul_le_mul_of_nonneg_left,
+    { simp_rw [←div_pow],
+      rw [←geom_sum_def, geom_sum_eq, div_le_iff_of_neg],
+      { transitivity (-1 : ℝ),
+        { linarith },
+        { simp only [neg_le_sub_iff_le_add, div_pow, nat.cast_succ, le_add_iff_nonneg_left],
+          exact div_nonneg (pow_nonneg (abs_nonneg x) k) (pow_nonneg (n+1).cast_nonneg k) } },
+      { linarith },
+      { linarith }, },
+    { exact div_nonneg (pow_nonneg (abs_nonneg x) n) (nat.cast_nonneg (n!)), }, },
+end
+
 lemma abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) :
   abs (exp x - 1) ≤ 2 * abs x :=
 calc abs (exp x - 1) = abs (exp x - ∑ m in range 1, x ^ m / m!) :

src/data/nat/factorial.lean

@@ -159,6 +159,18 @@ begin
   exact add_factorial_succ_le_factorial_add_succ i h,
 end
 
+lemma factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n! * n ^ (m - n) ≤ m! :=
+begin
+  suffices : n! * (n + 1) ^ (m - n) ≤ m!,
+  { apply trans _ this,
+    rw mul_le_mul_left,
+    apply pow_le_pow_of_le_left (zero_le n) (le_succ n),
+    exact factorial_pos n,},
+  convert nat.factorial_mul_pow_le_factorial,
+  exact (nat.add_sub_of_le hnm).symm,
+end
+
+
 end factorial
 
 /-! ### Ascending and descending factorials -/