internlm/Lean-Github huggingface dataset:
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 =
    (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
Tactic:
field_simp [← h, n.factorial_ne_zero]
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
⊢ (g x - g x₀) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) =
    (x - y) ^ 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 =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (g x - g x₀) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
ring
Proof state after:
no goals
Theorem: taylor_mean_remainder_central_aux
Proof state before:
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'
Tactic:
have h₁ : Icc x x₀ ⊆ Icc a b := Icc_subset_Icc hx.1 hx₀.2
Proof state after:
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₀
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.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₀
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.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₀
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.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₀
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.inr.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.inr.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.1.ne', _⟩
Proof state after:
case inr.inr.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.inr.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.inr.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 - f 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.inr.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 - f 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:
rw [← neg_sub, neg_mul, ← h]
Proof state after:
case inr.inr.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 - f x) * g' y
⊢ -((g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) 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.inr.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 - f x) * g' y
⊢ -((g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y) =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
field_simp [n.factorial_ne_zero]
Proof state after:
case inr.inr.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 - f x) * g' y
⊢ -((g x₀ - g x) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) * ↑n !) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y * ↑n !
Theorem: taylor_mean_remainder_central_aux
Proof state before:
case inr.inr.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 - f x) * g' y
⊢ -((g x₀ - g x) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) * ↑n !) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y * ↑n !
Tactic:
ring
Proof state after:
no goals
Theorem: taylor_mean_remainder_central
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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
obtain ⟨y, hy, hyx, h⟩ := taylor_mean_remainder_central_aux hab hx hx₀ hf hf' gcont gdiff
Proof state after:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'
Theorem: taylor_mean_remainder_central
Proof state before:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
refine' ⟨y, hy, _⟩
Proof state after:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Theorem: taylor_mean_remainder_central
Proof state before:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
rw [smul_eq_mul] at h
Proof state after:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Theorem: taylor_mean_remainder_central
Proof state before:
case intro.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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
rw [smul_eq_mul, div_mul_eq_mul_div, ← h, mul_div_cancel]
Proof state after:
case intro.intro.intro.h
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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ g' y ≠ 0
Theorem: taylor_mean_remainder_central
Proof state before:
case intro.intro.intro.h
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
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (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
⊢ g' y ≠ 0
Tactic:
exact g'_ne _ hy
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)
⊢ ∃ 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:
have gcont : ContinuousOn (fun t : ℝ => (x - t) ^ (n + 1)) (Icc a b) := by
  refine' Continuous.continuousOn _; continuity
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)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc 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 + 1) / ↑(n + 1)!
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)
⊢ ∃ 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:
rcases taylor_mean_remainder_central_aux hab hx hx₀ hf hf' gcont fun y _ =>
    monomial_has_deriv_aux y x _ with
  ⟨y, hy, hy', h⟩
Proof state after:
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
⊢ ∃ 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)!
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
⊢ ∃ 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:
have hy_ne : x - y ≠ 0 := sub_ne_zero_of_ne hy'.symm
Proof state after:
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)!