n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ abs' (exp 1 - expNear n 1 a₁) ≤ abs' 1 ^ n / ↑(Nat.factorial n) * b₁
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : ↑m = rm
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * rm)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * rm)
⊢ abs' (exp 1 - expNear n 1 a₁) ≤ abs' 1 ^ n / ↑(Nat.factorial n) * b₁
subst er
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ abs' (1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁) ≤ b₁ - abs' 1 / ↑m * (b₁ * ↑m)
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ abs' (exp 1 - expNear n 1 a₁) ≤ abs' 1 ^ n / ↑(Nat.factorial n) * b₁
refine' exp_approx_succ _ en _ _ _ h
no goals
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ abs' (1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁) ≤ b₁ - abs' 1 / ↑m * (b₁ * ↑m)
field_simp [show (m : ℝ) ≠ 0 by norm_cast; linarith]
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ ¬m = 0
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ ↑m ≠ 0
norm_cast
no goals
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : abs' (exp 1 - expNear m 1 ((a₁ - 1) * ↑m)) ≤ abs' 1 ^ m / ↑(Nat.factorial m) * (b₁ * ↑m)
⊢ ¬m = 0
linarith