x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
⊢ CauSeq.lim (cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) ≤
    ↑abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
⊢ ↑abs (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ ↑abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
rw [← lim_const (abv := Complex.abs) (∑ m in range n, _), exp, sub_eq_add_neg,
  ← lim_neg, lim_add, ← lim_abs]
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹))) j
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
⊢ CauSeq.lim (cauSeqAbs (exp' x + -const (↑abs) (∑ m in range n, x ^ m / ↑(Nat.factorial m)))) ≤
    ↑abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
refine' lim_le (CauSeq.le_of_exists ⟨n, fun j hj => _⟩)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹))) j
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹))) j
simp_rw [← sub_eq_add_neg]
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹))) j
show
  abs ((∑ m in range j, x ^ m / m.factorial) - ∑ m in range n, x ^ m / m.factorial) ≤
    abs x ^ n * ((n.succ : ℝ) * (n.factorial * n : ℝ)⁻¹)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑abs (∑ k in filter (fun k => n ≤ k) (range j), x ^ k / ↑(Nat.factorial k)) ≤
    ↑abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
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.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
rw [sum_range_sub_sum_range hj]
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ x ^ m / ↑(Nat.factorial m) = x ^ n * (x ^ (m - n) / ↑(Nat.factorial m))
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑abs (∑ m in filter (fun k => n ≤ k) (range j), x ^ m / ↑(Nat.factorial m)) =
    ↑abs (∑ m in filter (fun k => n ≤ k) (range j), x ^ n * (x ^ (m - n) / ↑(Nat.factorial m)))
refine' congr_arg abs (sum_congr rfl fun m hm => _)
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑(Nat.factorial m) = x ^ n * (x ^ (m - n) / ↑(Nat.factorial m))
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ x ^ m / ↑(Nat.factorial m) = x ^ n * (x ^ (m - n) / ↑(Nat.factorial m))
rw [mem_filter, mem_range] at hm
no goals
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑(Nat.factorial m) = x ^ n * (x ^ (m - n) / ↑(Nat.factorial m))
rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (↑abs (x ^ (x_1 - n)) / ↑(Nat.factorial x_1)) ≤
    ∑ x_1 in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (1 / ↑(Nat.factorial x_1))
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m in filter (fun k => n ≤ k) (range j), ↑abs (x ^ n * (x ^ (m - n) / ↑(Nat.factorial m))) ≤
    ∑ m in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (1 / ↑(Nat.factorial m))
simp_rw [map_mul, map_pow, map_div₀, abs_cast_nat]
case h.h.h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun k => n ≤ k) (range j)
⊢ ↑abs (x ^ (i✝ - n)) ≤ 1
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (↑abs (x ^ (x_1 - n)) / ↑(Nat.factorial x_1)) ≤
    ∑ x_1 in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (1 / ↑(Nat.factorial x_1))
gcongr
case h.h.h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun k => n ≤ k) (range j)
⊢ ↑abs x ^ (i✝ - n) ≤ 1
case h.h.h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun k => n ≤ k) (range j)
⊢ ↑abs (x ^ (i✝ - n)) ≤ 1
rw [abv_pow abs]
no goals
case h.h.h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun k => n ≤ k) (range j)
⊢ ↑abs x ^ (i✝ - n) ≤ 1
exact pow_le_one _ (abs.nonneg _) hx
no goals
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m in filter (fun k => n ≤ k) (range j), ↑abs x ^ n * (1 / ↑(Nat.factorial m)) =
    ↑abs x ^ n * ∑ m in filter (fun k => n ≤ k) (range j), 1 / ↑(Nat.factorial m)
simp [abs_mul, abv_pow abs, abs_div, mul_sum.symm]
case h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m in filter (fun k => n ≤ k) (range j), 1 / ↑(Nat.factorial m) ≤ ↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑abs x ^ n * ∑ m in filter (fun k => n ≤ k) (range j), 1 / ↑(Nat.factorial m) ≤
    ↑abs x ^ n * (↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹)
gcongr
no goals
case h
x : ℂ
hx : ↑abs x ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m in filter (fun k => n ≤ k) (range j), 1 / ↑(Nat.factorial m) ≤ ↑(Nat.succ n) * (↑(Nat.factorial n) * ↑n)⁻¹
exact sum_div_factorial_le _ _ hn