Theorem: exists_taylor_mean_remainder_bound_central (ExponentialRamsey/Prereq/Mathlib/Analysis/Calculus/Taylor.lean)

State before:
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
rcases eq_or_lt_of_le hab with (rfl | h)
State after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)

case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)

State before:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
let C := Sup ((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
State after:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)

State before:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
refine' ⟨C / (n + 1)!, fun x hx => _⟩
State after:
case inr
f : ℝ → ℝ
a b x₀ : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx₀ : x₀ ∈ Icc a b
h : a < b
C : Type := Sup ↑((fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖) '' Icc a b)
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ sorryAx ℝ true * |x - x₀| ^ (n + 1)

State before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1)
Tactic:
refine' ⟨0, fun x hx => _⟩
State after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)

State before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ ∈ Icc a a
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Tactic:
rw [Icc_self, mem_singleton_iff] at hx hx₀
State after:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ = a
x : ℝ
hx : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)

State before:
case inl
f : ℝ → ℝ
a x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx₀ : x₀ = a
x : ℝ
hx : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ 0 * |x - x₀| ^ (n + 1)
Tactic:
rw [hx₀, hx, taylorWithinEval_self, sub_self, MulZeroClass.zero_mul, norm_zero]
State after:
no goals