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

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

case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!

State before:
case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
have : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b) :=
  by
  refine'
    (hf.differentiable_on_iterated_deriv_within _ (uniqueDiffOn_Icc hab)).mono Ioo_subset_Icc_self
  rw [← Nat.cast_add_one, Nat.cast_lt]
  exact Nat.lt_succ_self _
State after:
case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!

State before:
case inr
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
obtain ⟨x', hx', h⟩ := taylor_mean_remainder_lagrange_central hab hx hx₀ hf.of_succ this
State after:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!

State before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖f x - taylorWithinEval f n (Icc a b) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [h, norm_div, norm_mul, Real.norm_coe_nat, Real.norm_eq_abs ((x - x₀) ^ _), ← abs_pow]
State after:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| / ↑(n + 1)! ≤ C * |(x - x₀) ^ (n + 1)| / ↑(n + 1)!

State before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| / ↑(n + 1)! ≤ C * |(x - x₀) ^ (n + 1)| / ↑(n + 1)!
Tactic:
refine' div_le_div_of_le (Nat.cast_nonneg _) _
State after:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| ≤ C * |(x - x₀) ^ (n + 1)|

State before:
case inr.intro.intro
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
this : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x' : ℝ
hx' : x' ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ‖iteratedDerivWithin (n + 1) f (Icc a b) x'‖ * |(x - x₀) ^ (n + 1)| ≤ C * |(x - x₀) ^ (n + 1)|
Tactic:
exact mul_le_mul_of_nonneg_right (hC _ hx') (abs_nonneg _)
State after:
no goals

State before:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hx₀ : x₀ ∈ Icc a a
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
simp only [Icc_self, mem_singleton_iff] at hx hx₀
State after:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx : x = a
hx₀ : x₀ = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!

State before:
case inl
f : ℝ → ℝ
a C x x₀ : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hC : ∀ y ∈ Ioo a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
hx : x = a
hx₀ : x₀ = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) x₀ x‖ ≤ C * |x - x₀| ^ (n + 1) / ↑(n + 1)!
Tactic:
substs hx₀ hx
State after:
case inl
f : ℝ → ℝ
C x : ℝ
n : ℕ
hab : x ≤ x
hf : ContDiffOn ℝ (↑n + 1) f (Icc x x)
hC : ∀ y ∈ Ioo x x, ‖iteratedDerivWithin (n + 1) f (Icc x x) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc x x) x x‖ ≤ C * |x - x| ^ (n + 1) / ↑(n + 1)!

State before:
case inl
f : ℝ → ℝ
C x : ℝ
n : ℕ
hab : x ≤ x
hf : ContDiffOn ℝ (↑n + 1) f (Icc x x)
hC : ∀ y ∈ Ioo x x, ‖iteratedDerivWithin (n + 1) f (Icc x x) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc x x) x x‖ ≤ C * |x - x| ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [taylorWithinEval_self, sub_self, sub_self, abs_zero, zero_pow Nat.succ_pos',
  MulZeroClass.mul_zero, zero_div, norm_zero]
State after:
no goals

State before:
f : ℝ → ℝ
a b C x x₀ : ℝ
n : ℕ
hab✝ : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hC : ∀ y ∈ Ioo a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
hab : a < b
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
Tactic:
refine'
  (hf.differentiable_on_iterated_deriv_within _ (uniqueDiffOn_Icc hab)).mono Ioo_subset_Icc_self
State after:
no goals