internlm/Lean-Github huggingface dataset:
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case intro.intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1))) • iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
use y, hy
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1))) • iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1))) • iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
dsimp at h
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [← eq_div_iff] at h
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ -(↑n + 1) * (x - y) ^ n ≠ 0
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ -(↑n + 1) * (x - y) ^ n ≠ 0
Tactic:
swap
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ -(↑n + 1) * (x - y) ^ n ≠ 0

case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
simp only [h, sub_self, zero_pow' _ (Nat.succ_ne_zero n), zero_sub, mul_neg, neg_mul,
  Nat.factorial_succ, Nat.cast_add_one, neg_div_neg_eq, Nat.cast_mul, field_simps]
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y / (↑n ! * ((↑n + 1) * (x - y) ^ n)) =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ((↑n + 1) * ↑n !)
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y / (↑n ! * ((↑n + 1) * (x - y) ^ n)) =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ((↑n + 1) * ↑n !)
Tactic:
rw [mul_left_comm, ← mul_assoc, ← div_div, div_eq_iff (pow_ne_zero _ hy_ne), div_mul_eq_mul_div]
Proof state after:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y / ((↑n + 1) * ↑n !) =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) * (x - y) ^ n / ((↑n + 1) * ↑n !)
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y / ((↑n + 1) * ↑n !) =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) * (x - y) ^ n / ((↑n + 1) * ↑n !)
Tactic:
congr 1
Proof state after:
case h.e_a
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) * (x - y) ^ n
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h.e_a
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) * (x - y) ^ n
Tactic:
ring_nf
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
Tactic:
refine' Continuous.continuousOn _
Proof state after:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ Continuous fun t => (x - t) ^ (n + 1)
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
case h
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ -(↑n + 1) * (x - y) ^ n ≠ 0
Tactic:
exact mul_ne_zero (neg_ne_zero.2 (by positivity)) (by positivity)
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ ↑n + 1 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_central
Proof state before:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ (x - y) ^ n ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)
Tactic:
rcases taylor_mean_remainder_central hab hx hx₀ hf hf' continuousOn_id
    (fun _ _ => hasDerivAt_id _) fun _ _ => by simp with
  ⟨y, hy, h⟩
Proof state after:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)
Tactic:
refine' ⟨y, hy, _⟩
Proof state after:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Tactic:
rw [h]
Proof state after:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Tactic:
field_simp [n.factorial_ne_zero]
Proof state after:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ (x - y) ^ n * (x - x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n * (x - x₀)
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
case intro.intro
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ (x - y) ^ n * (x - x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n * (x - x₀)
Tactic:
ring
Proof state after:
no goals
Theorem: taylor_mean_remainder_cauchy_central
Proof state before:
f : ℝ → ℝ
x x₀ a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioo a b
⊢ 1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: taylor_mean_remainder_bound_central
Proof 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)
Proof 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)!
Theorem: taylor_mean_remainder_bound_central
Proof 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 _
Proof 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)!
Theorem: taylor_mean_remainder_bound_central
Proof 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
Proof 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)!