[GOAL]
⊢ Tendsto (fun k => ∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero, ← tendsto_zero_iff_norm_tendsto_zero]
  -- (1) We introduce a useful sequence `u` of values in [0,1], then prove that another sequence
    --     constructed from `u` tends to `0` at `+∞`
[GOAL]
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
let u := fun k : ℕ => (k : NNReal) ^ (-1 / (2 * (k : ℝ) + 1))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
have H : Tendsto (fun k : ℕ => (1 : ℝ) - u k + u k ^ (2 * (k : ℝ) + 1)) atTop (𝓝 0) :=
  by
  convert
    (((tendsto_rpow_div_mul_add (-1) 2 1 two_ne_zero.symm).neg.const_add 1).add tendsto_inv_atTop_zero).comp
      tendsto_nat_cast_atTop_atTop using
    1
  · ext k
    simp only [NNReal.coe_nat_cast, Function.comp_apply, NNReal.coe_rpow]
    rw [← rpow_mul (Nat.cast_nonneg k) (-1 / (2 * (k : ℝ) + 1)) (2 * (k : ℝ) + 1),
      @div_mul_cancel _ _ (2 * (k : ℝ) + 1) _ (by norm_cast; simp only [Nat.succ_ne_zero, not_false_iff]),
      rpow_neg_one k, sub_eq_add_neg]
  ·
    simp only [add_zero, add_right_neg]
      -- (2) We convert the limit in our goal to an inequality
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
[PROOFSTEP]
convert
  (((tendsto_rpow_div_mul_add (-1) 2 1 two_ne_zero.symm).neg.const_add 1).add tendsto_inv_atTop_zero).comp
    tendsto_nat_cast_atTop_atTop using
  1
[GOAL]
case h.e'_3
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) = (fun x => 1 + -x ^ (-1 / (2 * x + 1)) + x⁻¹) ∘ Nat.cast
[PROOFSTEP]
ext k
[GOAL]
case h.e'_3.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1)) = ((fun x => 1 + -x ^ (-1 / (2 * x + 1)) + x⁻¹) ∘ Nat.cast) k
[PROOFSTEP]
simp only [NNReal.coe_nat_cast, Function.comp_apply, NNReal.coe_rpow]
[GOAL]
case h.e'_3.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 1 - ↑k ^ (-1 / (2 * ↑k + 1)) + (↑k ^ (-1 / (2 * ↑k + 1))) ^ (2 * ↑k + 1) = 1 + -↑k ^ (-1 / (2 * ↑k + 1)) + (↑k)⁻¹
[PROOFSTEP]
rw [← rpow_mul (Nat.cast_nonneg k) (-1 / (2 * (k : ℝ) + 1)) (2 * (k : ℝ) + 1),
  @div_mul_cancel _ _ (2 * (k : ℝ) + 1) _ (by norm_cast; simp only [Nat.succ_ne_zero, not_false_iff]), rpow_neg_one k,
  sub_eq_add_neg]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 2 * ↑k + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ ¬2 * k + 1 = 0
[PROOFSTEP]
simp only [Nat.succ_ne_zero, not_false_iff]
[GOAL]
case h.e'_5
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ 𝓝 0 = 𝓝 (1 + -1 + 0)
[PROOFSTEP]
simp only [add_zero, add_right_neg]
  -- (2) We convert the limit in our goal to an inequality
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero_norm _ H
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
⊢ ∀ (n : ℕ), ‖∑ i in Finset.range n, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u n) + ↑(u n ^ (2 * ↑n + 1))
[PROOFSTEP]
intro k
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let U := u k
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let b (i : ℕ) x := (-(1 : ℝ)) ^ i * x ^ (2 * i + 1) / (2 * i + 1)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let f x := arctan x - ∑ i in Finset.range k, b i x
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
suffices f_bound : |f 1 - f 0| ≤ (1 : ℝ) - U + U ^ (2 * (k : ℝ) + 1)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
rw [← norm_neg]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖-(∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4)‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
convert f_bound using 1
[GOAL]
case h.e'_3
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖-(∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4)‖ = |f 1 - f 0|
[PROOFSTEP]
simp
  -- We show that `U` is indeed in [0,1]
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hU1 : (U : ℝ) ≤ 1 := by
  by_cases hk : k = 0
  · simp [hk]
  ·
    exact
      rpow_le_one_of_one_le_of_nonpos (by norm_cast; exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk))
        (le_of_lt
          (@div_neg_of_neg_of_pos _ _ (-(1 : ℝ)) (2 * k + 1) (neg_neg_iff_pos.mpr zero_lt_one)
            (by norm_cast; exact Nat.succ_pos')))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ ↑U ≤ 1
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : k = 0
⊢ ↑U ≤ 1
[PROOFSTEP]
simp [hk]
[GOAL]
case neg
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ ↑U ≤ 1
[PROOFSTEP]
exact
  rpow_le_one_of_one_le_of_nonpos (by norm_cast; exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk))
    (le_of_lt
      (@div_neg_of_neg_of_pos _ _ (-(1 : ℝ)) (2 * k + 1) (neg_neg_iff_pos.mpr zero_lt_one)
        (by norm_cast; exact Nat.succ_pos')))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 1 ≤ ↑↑k
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 1 ≤ k
[PROOFSTEP]
exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 0 < 2 * ↑k + 1
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 0 < 2 * k + 1
[PROOFSTEP]
exact Nat.succ_pos'
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hU2 := NNReal.coe_nonneg U
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
let f' := fun x : ℝ => (-x ^ 2) ^ k / (1 + x ^ 2)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have has_deriv_at_f : ∀ x, HasDerivAt f (f' x) x := by
  intro x
  have has_deriv_at_b : ∀ i ∈ Finset.range k, HasDerivAt (b i) ((-x ^ 2) ^ i) x :=
    by
    intro i _
    convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
    · ext y
      simp only [id.def]
      ring
    · simp
      rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
        mul_pow (-1 : ℝ) (x ^ 2) i]
      ring_nf
  convert (hasDerivAt_arctan x).sub (HasDerivAt.sum has_deriv_at_b) using 1
  have g_sum := @geom_sum_eq _ _ (-x ^ 2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k
  simp only at g_sum ⊢
  rw [g_sum, ← neg_add' (x ^ 2) 1, add_comm (x ^ 2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq]
  ring
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
⊢ ∀ (x : ℝ), HasDerivAt f (f' x) x
[PROOFSTEP]
intro x
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
⊢ HasDerivAt f (f' x) x
[PROOFSTEP]
have has_deriv_at_b : ∀ i ∈ Finset.range k, HasDerivAt (b i) ((-x ^ 2) ^ i) x :=
  by
  intro i _
  convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
  · ext y
    simp only [id.def]
    ring
  · simp
    rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
      mul_pow (-1 : ℝ) (x ^ 2) i]
    ring_nf
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
⊢ ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
[PROOFSTEP]
intro i _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ HasDerivAt (b i) ((-x ^ 2) ^ i) x
[PROOFSTEP]
convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
[GOAL]
case h.e'_6
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ b i = fun y => (-1) ^ i / (2 * ↑i + 1) * id y ^ (2 * i + 1)
[PROOFSTEP]
ext y
[GOAL]
case h.e'_6.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
y : ℝ
⊢ b i y = (-1) ^ i / (2 * ↑i + 1) * id y ^ (2 * i + 1)
[PROOFSTEP]
simp only [id.def]
[GOAL]
case h.e'_6.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
y : ℝ
⊢ (-1) ^ i * y ^ (2 * i + 1) / (2 * ↑i + 1) = (-1) ^ i / (2 * ↑i + 1) * y ^ (2 * i + 1)
[PROOFSTEP]
ring
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1) ^ i / (2 * ↑i + 1) * (↑(2 * i + 1) * id x ^ (2 * i + 1 - 1) * 1)
[PROOFSTEP]
simp
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1) ^ i / (2 * ↑i + 1) * ((2 * ↑i + 1) * x ^ (2 * i))
[PROOFSTEP]
rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
  mul_pow (-1 : ℝ) (x ^ 2) i]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ 2 * ↑i + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ ¬2 * i + 1 = 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1 * x ^ 2) ^ i
[PROOFSTEP]
ring_nf
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
⊢ HasDerivAt f (f' x) x
[PROOFSTEP]
convert (hasDerivAt_arctan x).sub (HasDerivAt.sum has_deriv_at_b) using 1
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
⊢ f' x = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
have g_sum := @geom_sum_eq _ _ (-x ^ 2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ f' x = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
simp only at g_sum ⊢
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ (-x ^ 2) ^ k / (↑1 + x ^ 2) = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
rw [g_sum, ← neg_add' (x ^ 2) 1, add_comm (x ^ 2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq]
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ (-x ^ 2) ^ k / (↑1 + x ^ 2) = ↑1 / (↑1 + x ^ 2) + ((-x ^ 2) ^ k - 1) / (1 + x ^ 2)
[PROOFSTEP]
ring
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hderiv1 : ∀ x ∈ Icc (U : ℝ) 1, HasDerivWithinAt f (f' x) (Icc (U : ℝ) 1) x := fun x _ =>
  (has_deriv_at_f x).hasDerivWithinAt
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hderiv2 : ∀ x ∈ Icc 0 (U : ℝ), HasDerivWithinAt f (f' x) (Icc 0 (U : ℝ)) x := fun x _ =>
  (has_deriv_at_f x).hasDerivWithinAt
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have f'_bound : ∀ x ∈ Icc (-1 : ℝ) 1, |f' x| ≤ |x| ^ (2 * k) :=
  by
  intro x _
  rw [abs_div, IsAbsoluteValue.abv_pow abs (-x ^ 2) k, abs_neg, IsAbsoluteValue.abv_pow abs x 2, ← pow_mul]
  refine' div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _
  refine' le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _
  rw_mod_cast [abs_of_nonneg (add_nonneg zero_le_one (sq_nonneg x) : (0 : ℝ) ≤ _)]
  exact (le_add_of_nonneg_right (sq_nonneg x) : (1 : ℝ) ≤ _)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
⊢ ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
[PROOFSTEP]
intro x _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |f' x| ≤ |x| ^ (2 * k)
[PROOFSTEP]
rw [abs_div, IsAbsoluteValue.abv_pow abs (-x ^ 2) k, abs_neg, IsAbsoluteValue.abv_pow abs x 2, ← pow_mul]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |x| ^ (2 * k) / |↑1 + x ^ 2| ≤ |x| ^ (2 * k)
[PROOFSTEP]
refine' div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |x| ^ (2 * k) ≤ |x| ^ (2 * k) * |↑1 + x ^ 2|
[PROOFSTEP]
refine' le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ 1 ≤ |↑1 + x ^ 2|
[PROOFSTEP]
rw_mod_cast [abs_of_nonneg (add_nonneg zero_le_one (sq_nonneg x) : (0 : ℝ) ≤ _)]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * k + 1))) atTop (𝓝 0)
hU1 : U ≤ 1
hU2 : 0 ≤ U
a✝ : x ∈ Icc (↑(Int.negSucc 0)) 1
⊢ 1 ≤ 1 + x ^ 2
[PROOFSTEP]
exact (le_add_of_nonneg_right (sq_nonneg x) : (1 : ℝ) ≤ _)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hbound1 : ∀ x ∈ Ico (U : ℝ) 1, |f' x| ≤ 1 :=
  by
  rintro x ⟨hx_left, hx_right⟩
  have hincr := pow_le_pow_of_le_left (le_trans hU2 hx_left) (le_of_lt hx_right) (2 * k)
  rw [one_pow (2 * k), ← abs_of_nonneg (le_trans hU2 hx_left)] at hincr 
  rw [← abs_of_nonneg (le_trans hU2 hx_left)] at hx_right 
  linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_of_lt hx_right)))]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
⊢ ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
[PROOFSTEP]
rintro x ⟨hx_left, hx_right⟩
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
have hincr := pow_le_pow_of_le_left (le_trans hU2 hx_left) (le_of_lt hx_right) (2 * k)
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
hincr : x ^ (2 * k) ≤ 1 ^ (2 * k)
⊢ |f' x| ≤ 1
[PROOFSTEP]
rw [one_pow (2 * k), ← abs_of_nonneg (le_trans hU2 hx_left)] at hincr 
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
hincr : |x| ^ (2 * k) ≤ 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
rw [← abs_of_nonneg (le_trans hU2 hx_left)] at hx_right 
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : |x| < 1
hincr : |x| ^ (2 * k) ≤ 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_of_lt hx_right)))]
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hbound2 : ∀ x ∈ Ico 0 (U : ℝ), |f' x| ≤ U ^ (2 * k) :=
  by
  rintro x ⟨hx_left, hx_right⟩
  have hincr := pow_le_pow_of_le_left hx_left (le_of_lt hx_right) (2 * k)
  rw [← abs_of_nonneg hx_left] at hincr hx_right 
  rw [← abs_of_nonneg hU2] at hU1 hx_right 
  exact (f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))).trans hincr
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
⊢ ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rintro x ⟨hx_left, hx_right⟩
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : x < ↑U
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
have hincr := pow_le_pow_of_le_left hx_left (le_of_lt hx_right) (2 * k)
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : x < ↑U
hincr : x ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rw [← abs_of_nonneg hx_left] at hincr hx_right 
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : |x| < ↑U
hincr : |x| ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rw [← abs_of_nonneg hU2] at hU1 hx_right 
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : |↑U| ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : |x| < |↑U|
hincr : |x| ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
exact (f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))).trans hincr
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have mvt1 := norm_image_sub_le_of_norm_deriv_le_segment' hderiv1 hbound1 _ (right_mem_Icc.mpr hU1)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have mvt2 :=
  norm_image_sub_le_of_norm_deriv_le_segment' hderiv2 hbound2 _
    (right_mem_Icc.mpr hU2)
      -- The following algebra is enough to complete the proof
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
calc
  |f 1 - f 0| = |f 1 - f U + (f U - f 0)| := by simp
  _ ≤ 1 * (1 - U) + U ^ (2 * k) * (U - 0) := (le_trans (abs_add (f 1 - f U) (f U - f 0)) (add_le_add mvt1 mvt2))
  _ = 1 - U + (U : ℝ) ^ (2 * k) * U := by simp
  _ = 1 - u k + u k ^ (2 * (k : ℝ) + 1) := by rw [← pow_succ' (U : ℝ) (2 * k)]; norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ |f 1 - f 0| = |f 1 - f ↑U + (f ↑U - f 0)|
[PROOFSTEP]
simp
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 * (1 - ↑U) + ↑(U ^ (2 * k)) * (↑U - 0) = 1 - ↑U + ↑U ^ (2 * k) * ↑U
[PROOFSTEP]
simp
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 - ↑U + ↑U ^ (2 * k) * ↑U = 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
rw [← pow_succ' (U : ℝ) (2 * k)]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 - ↑U + ↑U ^ (2 * k + 1) = 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
norm_cast
