x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ↑(cos x - (1 - x ^ 2 / 2)) = ↑Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2))
x : ℝ
hx : abs' x ≤ 1
⊢ abs' (cos x - (1 - x ^ 2 / 2)) = ↑Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2))
rw [← abs_ofReal]
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ↑(cos x - (1 - x ^ 2 / 2)) = ↑Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2))
simp
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.cos ↑x - (1 - ↑x ^ 2 / 2)) =
    ↑Complex.abs ((Complex.exp (↑x * I) + Complex.exp (-↑x * I) - (2 - ↑x ^ 2)) / 2)
simp [Complex.cos, sub_div, add_div, neg_div, div_self (two_ne_zero' ℂ)]
x : ℝ
hx : abs' x ≤ 1
⊢ Complex.exp (↑x * I) + Complex.exp (-↑x * I) - (2 - ↑x ^ 2) =
    Complex.exp (↑x * I) -
        (∑ m in range 0, (↑x * I) ^ m / ↑(Nat.factorial m) + (↑x * I) ^ 0 / ↑(Nat.factorial 0) +
              (↑x * I) ^ 1 / ↑(Nat.factorial 1) +
            (↑x * I) ^ 2 / ↑(Nat.factorial 2) +
          (↑x * I) ^ 3 / ↑(Nat.factorial 3)) +
      (Complex.exp (-↑x * I) -
        (∑ m in range 0, (-↑x * I) ^ m / ↑(Nat.factorial m) + (-↑x * I) ^ 0 / ↑(Nat.factorial 0) +
              (-↑x * I) ^ 1 / ↑(Nat.factorial 1) +
            (-↑x * I) ^ 2 / ↑(Nat.factorial 2) +
          (-↑x * I) ^ 3 / ↑(Nat.factorial 3)))
x : ℝ
hx : abs' x ≤ 1
⊢ Complex.exp (↑x * I) + Complex.exp (-↑x * I) - (2 - ↑x ^ 2) =
    Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m) +
      (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m))
simp only [sum_range_succ]
x : ℝ
hx : abs' x ≤ 1
⊢ Complex.exp (↑x * I) + Complex.exp (-(↑x * I)) - (2 - ↑x * ↑x) =
    Complex.exp (↑x * I) -
        (1 + ↑x * I + ↑x * I * (↑x * I) / (1 + 1) + ↑x * I * (↑x * I * (↑x * I)) / ((2 + 1) * (1 + 1))) +
      (Complex.exp (-(↑x * I)) -
        (1 + -(↑x * I) + ↑x * I * (↑x * I) / (1 + 1) + -(↑x * I * (↑x * I * (↑x * I))) / ((2 + 1) * (1 + 1))))
x : ℝ
hx : abs' x ≤ 1
⊢ Complex.exp (↑x * I) + Complex.exp (-↑x * I) - (2 - ↑x ^ 2) =
    Complex.exp (↑x * I) -
        (∑ m in range 0, (↑x * I) ^ m / ↑(Nat.factorial m) + (↑x * I) ^ 0 / ↑(Nat.factorial 0) +
              (↑x * I) ^ 1 / ↑(Nat.factorial 1) +
            (↑x * I) ^ 2 / ↑(Nat.factorial 2) +
          (↑x * I) ^ 3 / ↑(Nat.factorial 3)) +
      (Complex.exp (-↑x * I) -
        (∑ m in range 0, (-↑x * I) ^ m / ↑(Nat.factorial m) + (-↑x * I) ^ 0 / ↑(Nat.factorial 0) +
              (-↑x * I) ^ 1 / ↑(Nat.factorial 1) +
            (-↑x * I) ^ 2 / ↑(Nat.factorial 2) +
          (-↑x * I) ^ 3 / ↑(Nat.factorial 3)))
simp [pow_succ]
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ Complex.exp (↑x * I) + Complex.exp (-(↑x * I)) - (2 - ↑x * ↑x) =
    Complex.exp (↑x * I) -
        (1 + ↑x * I + ↑x * I * (↑x * I) / (1 + 1) + ↑x * I * (↑x * I * (↑x * I)) / ((2 + 1) * (1 + 1))) +
      (Complex.exp (-(↑x * I)) -
        (1 + -(↑x * I) + ↑x * I * (↑x * I) / (1 + 1) + -(↑x * I * (↑x * I * (↑x * I))) / ((2 + 1) * (1 + 1))))
apply Complex.ext <;> simp [div_eq_mul_inv, normSq] <;> ring_nf
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs
      ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2 +
        (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2) ≤
    ↑Complex.abs ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2) +
      ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2)
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs
      ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m) +
          (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m))) /
        2) ≤
    ↑Complex.abs ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2) +
      ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2)
rw [add_div]
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs
      ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2 +
        (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2) ≤
    ↑Complex.abs ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2) +
      ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2)
exact Complex.abs.add_le _ _
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2) +
      ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2) =
    ↑Complex.abs (Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2 +
      ↑Complex.abs (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2
simp [map_div₀]
case h₁.h
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) ≤
    ↑Complex.abs (↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)

case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) ≤
    ↑Complex.abs (-↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) / 2 +
      ↑Complex.abs (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) / 2 ≤
    ↑Complex.abs (↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ↑Complex.abs (-↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2
gcongr
no goals
case h₁.h
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) ≤
    ↑Complex.abs (↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)
exact Complex.exp_bound (by simpa) (by decide)
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (↑x * I) ≤ 1
simpa
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ 0 < 4
decide
no goals
case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) ≤
    ↑Complex.abs (-↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)
exact Complex.exp_bound (by simpa) (by decide)
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (-↑x * I) ≤ 1
simpa
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ 0 < 4
decide
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ↑Complex.abs (-↑x * I) ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 ≤
    abs' x ^ 4 * (5 / 96)
norm_num