x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
⊢ CauSeq.lim (cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
⊢ ↑abs (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ ↑abs x ^ n / ↑(Nat.factorial n) * 2
rw [← lim_const (abv := Complex.abs) (∑ m in range n, _),
  exp, sub_eq_add_neg, ← lim_neg, lim_add, ← lim_abs]
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) j ≤
    ↑(const abs' (↑abs x ^ n / ↑(Nat.factorial n) * 2)) j
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
⊢ CauSeq.lim (cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
refine' lim_le (CauSeq.le_of_exists ⟨n, fun j hj => _⟩)
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqAbs (exp' x - const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) j ≤
    ↑(const abs' (↑abs x ^ n / ↑(Nat.factorial n) * 2)) j
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) j ≤
    ↑(const abs' (↑abs x ^ n / ↑(Nat.factorial n) * 2)) j
simp_rw [← sub_eq_add_neg]
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqAbs (exp' x - const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) j ≤
    ↑(const abs' (↑abs x ^ n / ↑(Nat.factorial n) * 2)) j
show abs ((∑ m in range j, x ^ m / m.factorial) - ∑ m in range n, x ^ m / m.factorial) ≤
  abs x ^ n / n.factorial * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
k : ℕ := j - n
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
let k := j - n
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj : j ≥ n
k : ℕ := j - n
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
have hj : j = n + k := (add_tsub_cancel_of_le hj).symm
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs (∑ k in range k, x ^ (n + k) / ↑(Nat.factorial (n + k))) ≤ ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs (∑ m in range j, x ^ m / ↑(Nat.factorial m) - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
rw [hj, sum_range_add_sub_sum_range]
case calc_1
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ (n + i) / ↑(Nat.factorial (n + i)) ≤
    ∑ i in range k, ↑abs x ^ (n + i) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ i)

case calc_2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ (n + i) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ i) =
    ∑ i in range k, ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ i / ↑(Nat.succ n) ^ i)

case calc_3
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ i / ↑(Nat.succ n) ^ i) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs (∑ k in range k, x ^ (n + k) / ↑(Nat.factorial (n + k))) ≤ ↑abs x ^ n / ↑(Nat.factorial n) * 2
calc
  abs (∑ i : ℕ in range k, x ^ (n + i) / ((n + i).factorial : ℂ)) ≤
      ∑ i : ℕ in range k, abs (x ^ (n + i) / ((n + i).factorial : ℂ)) :=
    abv_sum_le_sum_abv _ _
  _ ≤ ∑ i : ℕ in range k, abs x ^ (n + i) / (n + i).factorial := by
    simp [Complex.abs_cast_nat, map_div₀, abv_pow abs]
  _ ≤ ∑ i : ℕ in range k, abs x ^ (n + i) / ((n.factorial : ℝ) * (n.succ : ℝ) ^ i) := ?_
  _ = ∑ i : ℕ in range k, abs x ^ n / n.factorial * (abs x ^ i / (n.succ : ℝ) ^ i) := ?_
  _ ≤ abs x ^ n / ↑n.factorial * 2 := ?_
no goals
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs (x ^ (n + i) / ↑(Nat.factorial (n + i))) ≤
    ∑ i in range k, ↑abs x ^ (n + i) / ↑(Nat.factorial (n + i))
simp [Complex.abs_cast_nat, map_div₀, abv_pow abs]
case calc_1.h.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
i✝ : ℕ
a✝ : i✝ ∈ range k
⊢ ↑(Nat.factorial n) * ↑(Nat.succ n) ^ i✝ ≤ ↑(Nat.factorial (n + i✝))
case calc_1
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ (n + i) / ↑(Nat.factorial (n + i)) ≤
    ∑ i in range k, ↑abs x ^ (n + i) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ i)
gcongr
no goals
case calc_1.h.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
i✝ : ℕ
a✝ : i✝ ∈ range k
⊢ ↑(Nat.factorial n) * ↑(Nat.succ n) ^ i✝ ≤ ↑(Nat.factorial (n + i✝))
exact_mod_cast Nat.factorial_mul_pow_le_factorial
case calc_2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
x✝¹ : ℕ
x✝ : x✝¹ ∈ range k
⊢ ↑abs x ^ (n + x✝¹) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ x✝¹) =
    ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ x✝¹ / ↑(Nat.succ n) ^ x✝¹)
case calc_2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ (n + i) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ i) =
    ∑ i in range k, ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ i / ↑(Nat.succ n) ^ i)
refine' Finset.sum_congr rfl fun _ _ => _
no goals
case calc_2
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
x✝¹ : ℕ
x✝ : x✝¹ ∈ range k
⊢ ↑abs x ^ (n + x✝¹) / (↑(Nat.factorial n) * ↑(Nat.succ n) ^ x✝¹) =
    ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ x✝¹ / ↑(Nat.succ n) ^ x✝¹)
simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]
case calc_3
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x ^ n / ↑(Nat.factorial n) * ∑ x_1 in range k, ↑abs x ^ x_1 / ↑(Nat.succ n) ^ x_1 ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
case calc_3
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i in range k, ↑abs x ^ n / ↑(Nat.factorial n) * (↑abs x ^ i / ↑(Nat.succ n) ^ i) ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
rw [← mul_sum]
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 in range k, ↑abs x ^ x_1 / ↑(Nat.succ n) ^ x_1 ≤ 2
case calc_3
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x ^ n / ↑(Nat.factorial n) * ∑ x_1 in range k, ↑abs x ^ x_1 / ↑(Nat.succ n) ^ x_1 ≤
    ↑abs x ^ n / ↑(Nat.factorial n) * 2
gcongr
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 in range (j - n), (↑abs x / ↑(Nat.succ n)) ^ x_1 ≤ 2
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 in range k, ↑abs x ^ x_1 / ↑(Nat.succ n) ^ x_1 ≤ 2
simp_rw [← div_pow]
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (↑abs x / ↑(Nat.succ n) - 1) ≤ (↑abs x / ↑(Nat.succ n)) ^ (j - n) - 1

case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x / ↑(Nat.succ n) - 1 < 0

case calc_3.h.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x / ↑(Nat.succ n) ≠ 1
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 in range (j - n), (↑abs x / ↑(Nat.succ n)) ^ x_1 ≤ 2
rw [geom_sum_eq, div_le_iff_of_neg]
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (↑abs x / ↑(Nat.succ n) - 1) ≤ -1

x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ -1 ≤ (↑abs x / ↑(Nat.succ n)) ^ (j - n) - 1
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (↑abs x / ↑(Nat.succ n) - 1) ≤ (↑abs x / ↑(Nat.succ n)) ^ (j - n) - 1
trans (-1 : ℝ)
no goals
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (↑abs x / ↑(Nat.succ n) - 1) ≤ -1
linarith
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 0 ≤ ↑abs x ^ (j - n) / (↑n + 1) ^ (j - n)
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ -1 ≤ (↑abs x / ↑(Nat.succ n)) ^ (j - n) - 1
simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
no goals
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 0 ≤ ↑abs x ^ (j - n) / (↑n + 1) ^ (j - n)
positivity
no goals
case calc_3.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x / ↑(Nat.succ n) - 1 < 0
linarith
no goals
case calc_3.h.h
x : ℂ
n : ℕ
hx : ↑abs x / ↑(Nat.succ n) ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ↑abs x / ↑(Nat.succ n) ≠ 1
linarith