x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ↑(sin x - (x - x ^ 3 / 6)) = ↑Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6))
x : ℝ
hx : abs' x ≤ 1
⊢ abs' (sin x - (x - x ^ 3 / 6)) = ↑Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6))
rw [← abs_ofReal]
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs ↑(sin x - (x - x ^ 3 / 6)) = ↑Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6))
simp
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs (Complex.sin ↑x - ↑(x - x ^ 3 / 6)) =
    ↑Complex.abs (((Complex.exp (-↑x * I) - Complex.exp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 3)) / 2)
simp [Complex.sin, sub_div, add_div, neg_div, mul_div_cancel_left _ (two_ne_zero' ℂ), div_div,
  show (3 : ℂ) * 2 = 6 by norm_num]
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ 3 * 2 = 6
norm_num
x : ℝ
hx : abs' x ≤ 1
⊢ (Complex.exp (-↑x * I) - Complex.exp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 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)) -
        (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)))) *
      I
x : ℝ
hx : abs' x ≤ 1
⊢ (Complex.exp (-↑x * I) - Complex.exp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 3) =
    (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))) *
      I
simp only [sum_range_succ]
x : ℝ
hx : abs' x ≤ 1
⊢ (Complex.exp (-(↑x * I)) - Complex.exp (↑x * I)) * I - (2 * ↑x - ↑x * (↑x * ↑x) / 3) =
    (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))))) *
      I
x : ℝ
hx : abs' x ≤ 1
⊢ (Complex.exp (-↑x * I) - Complex.exp (↑x * I)) * I - ↑(2 * x - x ^ 3 / 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)) -
        (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)))) *
      I
simp [pow_succ]
case a
x : ℝ
hx : abs' x ≤ 1
⊢ sin x - (Complex.exp (-(↑x * I))).im - (2 * x - x * (x * x) * 3⁻¹) =
    sin x - (x + -(x * (x * x) * ((1 + 1)⁻¹ * ((2 + 1) * ((2 + 1)⁻¹ * (2 + 1)⁻¹))))) -
      ((Complex.exp (-(↑x * I))).im - (-x + x * (x * x) * ((1 + 1)⁻¹ * ((2 + 1) * ((2 + 1)⁻¹ * (2 + 1)⁻¹)))))
x : ℝ
hx : abs' x ≤ 1
⊢ (Complex.exp (-(↑x * I)) - Complex.exp (↑x * I)) * I - (2 * ↑x - ↑x * (↑x * ↑x) / 3) =
    (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))))) *
      I
apply Complex.ext <;> simp [div_eq_mul_inv, normSq]
no goals
case a
x : ℝ
hx : abs' x ≤ 1
⊢ sin x - (Complex.exp (-(↑x * I))).im - (2 * x - x * (x * x) * 3⁻¹) =
    sin x - (x + -(x * (x * x) * ((1 + 1)⁻¹ * ((2 + 1) * ((2 + 1)⁻¹ * (2 + 1)⁻¹))))) -
      ((Complex.exp (-(↑x * I))).im - (-x + x * (x * x) * ((1 + 1)⁻¹ * ((2 + 1) * ((2 + 1)⁻¹ * (2 + 1)⁻¹)))))
ring
x : ℝ
hx : abs' x ≤ 1
⊢ ↑Complex.abs
      ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) * I / 2 +
        -((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 2) ≤
    ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) * I / 2) +
      ↑Complex.abs (-((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 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))) *
          I /
        2) ≤
    ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) * I / 2) +
      ↑Complex.abs (-((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 2)
rw [sub_mul, sub_eq_add_neg, 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)) * I / 2 +
        -((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 2) ≤
    ↑Complex.abs ((Complex.exp (-↑x * I) - ∑ m in range 4, (-↑x * I) ^ m / ↑(Nat.factorial m)) * I / 2) +
      ↑Complex.abs (-((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 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)) * I / 2) +
      ↑Complex.abs (-((Complex.exp (↑x * I) - ∑ m in range 4, (↑x * I) ^ m / ↑(Nat.factorial m)) * I) / 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 [add_comm, 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