[Merged by Bors] - feat(data/complex/exponential): bound on exp for arbitrary arguments

src/algebra/big_operators/basic.lean

@@ -776,6 +776,16 @@ 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) :=
+begin
+  rw [prod_range_add f n m, div_eq_mul_inv],
+  simp,
+end
+
+
 @[to_additive]
 lemma prod_range_zero (f : ℕ → β) :
   ∏ k in range 0, f k = 1 :=

src/data/complex/exponential.lean

@@ -1279,17 +1279,76 @@ 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,
+    exact (nat.add_sub_of_le hj).symm,
+  rw hj,
+  rw sum_range_add_sub_sum_range,
+  calc abs (∑ (k : ℕ) in range k, x ^ (n + k) / ((n + k)! : ℂ))
+      ≤ ∑ (k : ℕ) in range k, abs (x ^ (n + k) / ((n + k)! : ℂ)) : abv_sum_le_sum_abv _ _
+  ... ≤ ∑ (k : ℕ) in range k, (abs x) ^ (n + k) / (n + k)! :
+          begin
+            refine sum_le_sum (λ m hm, _),
+            simp only [complex.abs_cast_nat, complex.abs_div],
+            rw [abv_pow abs],
+          end
+  ... ≤ ∑ (k : ℕ) in range k, (abs x) ^ (n + k) / (n! * n.succ ^ k) :
+          begin
+            refine sum_le_sum (λ m hm, _),
+            apply div_le_div (pow_nonneg (abs_nonneg x) (n + m)) (le_refl _),
+            { apply mul_pos,
+              { rw nat.cast_pos,
+                exact nat.factorial_pos n,},
+              { apply pow_pos,
+                rw nat.cast_pos,
+                exact nat.succ_pos n,},},
+            { rw [←nat.cast_pow, ←nat.cast_mul, nat.cast_le],
+              exact (nat.factorial_mul_pow_le_factorial),},
+          end
+  ... = ∑ (k : ℕ) in range k, (abs x) ^ (n) / (n!) * ((abs x)^k / n.succ ^ k) :
+          begin
+            congr,
+            funext,
+            simp only [pow_add, div_eq_inv_mul, mul_inv'],
+            ring,
+          end
+  ... ≤ abs x ^ n / (↑n!) * 2 :
+          begin
+            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],
+                  apply div_nonneg (pow_nonneg (abs_nonneg x) k)
+                                   (pow_nonneg (nat.cast_nonneg (n + 1)) k),},},
+              { linarith,},
+              { linarith,},},
+            { exact div_nonneg (pow_nonneg (abs_nonneg x) n) (nat.cast_nonneg (n!)),},
+          end,
+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 -/