internlm/Lean-Github huggingface dataset:
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
Proof state after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
Proof state after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (uIcc x₀ x) y =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (uIcc x₀ x) y =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
field_simp [n.cast_add_one_ne_zero, n.factorial_ne_zero, xy_ne y hy]
Proof state after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * ↑(n + 1)! =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) * (↑n ! * ((↑n + 1) * (x - y) ^ n))
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * ↑(n + 1)! =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) * (↑n ! * ((↑n + 1) * (x - y) ^ n))
Tactic:
ring_nf
Proof state after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑(1 + n)! * (x - y) ^ n * (x - x₀) ^ n -
      x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑(1 + n)! * (x - y) ^ n * (x - x₀) ^ n =
    x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * ↑n * (x - y) ^ n * (x - x₀) ^ n +
        x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * (x - y) ^ n * (x - x₀) ^ n +
      (-(x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * ↑n * (x - y) ^ n * (x - x₀) ^ n) -
        x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * (x - y) ^ n * (x - x₀) ^ n)
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
Tactic:
refine' Continuous.continuousOn _
Proof state after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ Continuous fun t => (x - t) ^ (n + 1)
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ Continuous fun t => (x - t) ^ (n + 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
⊢ ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
Tactic:
intro y hy
Proof state after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ (x - y) ^ n ≠ 0
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ (x - y) ^ n ≠ 0
Tactic:
refine' pow_ne_zero _ _
Proof state after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x - y ≠ 0
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x - y ≠ 0
Tactic:
rw [sub_ne_zero]
Proof state after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x ≠ y
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x ≠ y
Tactic:
cases' le_total x₀ x with h h
Proof state after:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x₀ ≤ x
⊢ x ≠ y

case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x ≤ x₀
⊢ x ≠ y
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x₀ ≤ x
⊢ x ≠ y
Tactic:
rw [uIoo_of_le h] at hy
Proof state after:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
h : x₀ ≤ x
⊢ x ≠ y
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
h : x₀ ≤ x
⊢ x ≠ y
Tactic:
exact hy.2.ne'
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x ≤ x₀
⊢ x ≠ y
Tactic:
rw [uIoo_of_ge h] at hy
Proof state after:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x x₀
h : x ≤ x₀
⊢ x ≠ y
Theorem: taylor_mean_remainder_lagrange_unordered
Proof state before:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x x₀
h : x ≤ x₀
⊢ x ≠ y
Tactic:
exact hy.1.ne
Proof state after:
no goals
Theorem: taylor_mean_remainder_central_aux
Proof state before:
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
rcases eq_or_ne x₀ x with (rfl | hx')
Proof state after:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx : x₀ ∈ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x₀ ∧
        (f x₀ - taylorWithinEval f n (Icc a b) x₀ x₀) * g' x' =
          ((x₀ - x') ^ n / ↑n ! * (g x₀ - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

case inr
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx' : x₀ ≠ x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx' : x₀ ≠ x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
rcases Ne.lt_or_lt hx' with (hx' | hx')
Proof state after:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

case inr.inr
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx : x₀ ∈ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x₀ ∧
        (f x₀ - taylorWithinEval f n (Icc a b) x₀ x₀) * g' x' =
          ((x₀ - x') ^ n / ↑n ! * (g x₀ - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
simp only [sub_self, taylorWithinEval_self, MulZeroClass.mul_zero, zero_div, zero_smul,
  eq_self_iff_true, exists_prop, and_true_iff, MulZeroClass.zero_mul]
Proof state after:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx : x₀ ∈ Icc a b
⊢ ∃ x' ∈ Ioo a b, x' ≠ x₀
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx : x₀ ∈ Icc a b
⊢ ∃ x' ∈ Ioo a b, x' ≠ x₀
Tactic:
obtain ⟨x', hx'⟩ := ((Ioo_infinite hab).diffₓ (Set.finite_singleton x₀)).Nonempty
Proof state after:
no goals
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₁ : Icc x₀ x ⊆ Icc a b := Icc_subset_Icc hx₀.1 hx.2
Proof state after:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₂ : Ioo x₀ x ⊆ Ioo a b := Ioo_subset_Ioo hx₀.1 hx.2
Proof state after:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inl
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
obtain ⟨y, hy, h⟩ :=
  exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc a b) t x)
    (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) hx'
    ((continuousOn_taylorWithinEval (uniqueDiffOn_Icc hab) hf).mono h₁)
    (fun _ hy => taylorWithinEval_hasDerivAt_Ioo _ hab (h₂ hy) hf hf') g g' (gcont.mono h₁)
    fun y hy => gdiff y (h₂ hy)
Proof state after:
case inr.inl.intro.intro
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inl.intro.intro
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
refine' ⟨y, h₂ hy, hy.2.Ne, _⟩
Proof state after:
case inr.inl.intro.intro
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inl.intro.intro
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
simp only [taylorWithinEval_self] at h
Proof state after:
case inr.inl.intro.intro
f g g' : ℝ → ℝ
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 g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y