case inl
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ (y : ℝ), y ∈ Icc a a → ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !

case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
rcases eq_or_lt_of_le hab with (rfl | h)
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b) :=
  hf.differentiableOn_iteratedDerivWithin (WithTop.coe_lt_coe.mpr n.lt_succ_self)
    (uniqueDiffOn_Icc h)
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
have h' : ∀ (y : ℝ) (_ : y ∈ Ico a x),
    ‖((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤
      (n ! : ℝ)⁻¹ * |x - a| ^ n * C := by
  rintro y ⟨hay, hyx⟩
  rw [norm_smul, Real.norm_eq_abs]
  refine' mul_le_mul _ (hC y ⟨hay, hyx.le.trans hx.2⟩) (by positivity) (by positivity)
  rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
  gcongr
  rw [abs_of_nonneg, abs_of_nonneg] <;> linarith
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
have A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
    (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t := by
  intro t ht
  have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
  exact (has_deriv_within_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this :
  ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1)
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this :
  ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
simp only [taylorWithinEval_self] at this
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
refine' this.trans_eq _
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ (↑n !)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
rw [abs_of_nonneg (sub_nonneg.mpr hx.1)]
no goals
case inr
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
A :
  ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C * (x - a)
⊢ (↑n !)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
ring
case inl
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x = a
hC : ∀ (y : ℝ), y ∈ Icc a a → ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
case inl
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ (y : ℝ), y ∈ Icc a a → ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
rw [Icc_self, mem_singleton_iff] at hx
no goals
case inl
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x = a
hC : ∀ (y : ℝ), y ∈ Icc a a → ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
simp [hx]
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
rintro y ⟨hay, hyx⟩
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs ((↑n !)⁻¹ * (x - y) ^ n) * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
rw [norm_smul, Real.norm_eq_abs]
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs ((↑n !)⁻¹ * (x - y) ^ n) ≤ (↑n !)⁻¹ * abs (x - a) ^ n
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs ((↑n !)⁻¹ * (x - y) ^ n) * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
refine' mul_le_mul _ (hC y ⟨hay, hyx.le.trans hx.2⟩) (by positivity) (by positivity)
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ (↑n !)⁻¹ * abs (x - y) ^ n ≤ (↑n !)⁻¹ * abs (x - a) ^ n
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs ((↑n !)⁻¹ * (x - y) ^ n) ≤ (↑n !)⁻¹ * abs (x - a) ^ n
rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
case intro.h.hab
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs (x - y) ≤ abs (x - a)
case intro
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ (↑n !)⁻¹ * abs (x - y) ^ n ≤ (↑n !)⁻¹ * abs (x - a) ^ n
gcongr
no goals
case intro.h.hab
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ abs (x - y) ≤ abs (x - a)
rw [abs_of_nonneg, abs_of_nonneg] <;> linarith
no goals
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ 0 ≤ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
positivity
no goals
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ 0 ≤ (↑n !)⁻¹ * abs (x - a) ^ n
positivity
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
t : ℝ
ht : t ∈ Icc a x
⊢ HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
    (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
⊢ ∀ (t : ℝ),
    t ∈ Icc a x →
      HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
        (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
intro t ht
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
t : ℝ
ht : t ∈ Icc a x
I : Icc a x ⊆ Icc a b
⊢ HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
    (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
t : ℝ
ht : t ∈ Icc a x
⊢ HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
    (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
no goals
𝕜 : Type ?u.342431
E : Type u_1
F : Type ?u.342437
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ (y : ℝ), y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ (y : ℝ),
    y ∈ Ico a x →
      ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * abs (x - a) ^ n * C
t : ℝ
ht : t ∈ Icc a x
I : Icc a x ⊆ Icc a b
⊢ HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
    (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
exact (has_deriv_within_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I