hasDerivWithinAt_taylorWithinEval
theorem hasDerivWithinAt_taylorWithinEval :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x y : ℝ} {n : ℕ}
{s s' : Set ℝ},
UniqueDiffWithinAt ℝ s' y →
UniqueDiffOn ℝ s →
s' ∈ nhdsWithin y s →
y ∈ s' →
s' ⊆ s →
ContDiffOn ℝ (↑n) f s →
DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y →
HasDerivWithinAt (fun t => taylorWithinEval f n s t x)
(((↑n.factorial)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
This theorem states that for a real-valued function `f` and given real numbers `x` and `y`, the derivative of the Taylor polynomial of `f` with respect to `x₀` can be calculated within an arbitrary set. Specifically, if `s'` is a unique differentiation point within the set `s` at `y`, and `s'` is a neighborhood subset of `s` at `y`, and `y` is in `s'`, and `s'` is a subset of `s`, and `f` is continuously differentiable up to the `n`-th derivative on `s`, and the `n`-th iterated derivative of `f` is differentiable within `s` at `y`, then the function has a derivative within `s'` at `y`. This derivative is equal to the product of the inverse of the factorial of `n` and the `n`-th power of the difference of `x` and `y`, all scaled by the `(n + 1)`-th iterated derivative of `f` within `s` at `y`.
More concisely: If `f` is a real-valued function that is continuously differentiable up to the `n`-th derivative on a set `s` containing `x₀`, `y`, and `s'` is a neighborhood subset of `s` at `y` where `f` and its first `n+1` derivatives are defined and differentiable, then the derivative of the `n`-th degree Taylor polynomial of `f` at `x₀` with respect to `y` is equal to the `(n+1)`-th iterated derivative of `f` at `y` multiplied by the scaling factor `(x - y) / n!`.
|
monomial_has_deriv_aux
theorem monomial_has_deriv_aux :
∀ (t x : ℝ) (n : ℕ), HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t
This theorem states that for all real numbers `t` and `x`, and for all natural numbers `n`, the function `y => (x - y) ^ (n + 1)` has a derivative at the point `t`. The derivative at this point is given by `-(↑n + 1) * (x - t) ^ n`. This is a helper lemma used in the calculation of the derivative of the monomial that appears in Taylor expansions.
More concisely: For all real numbers `x` and `t`, and natural numbers `n`, the `n`th derivative of the function `x => (x - t) ^ (n + 1)` exists and is equal to `-(n + 1) * (x - t) ^ n`.
|
taylor_mean_remainder
theorem taylor_mean_remainder :
∀ {f g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
x₀ < x →
ContDiffOn ℝ (↑n) f (Set.Icc x₀ x) →
DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x) →
ContinuousOn g (Set.Icc x₀ x) →
(∀ x_1 ∈ Set.Ioo x₀ x, HasDerivAt g (g' x_1) x_1) →
(∀ x_1 ∈ Set.Ioo x₀ x, g' x_1 ≠ 0) →
∃ x' ∈ Set.Ioo x₀ x,
f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x =
((x - x') ^ n / ↑n.factorial * (g x - g x₀) / g' x') •
iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x'
The theorem stated is known as **Taylor's theorem** with a general mean value form of the remainder. In simple terms, it states that if a function `f` is `n+1`-times continuously differentiable in a closed interval between `x₀` and `x` (inclusive), and `n+1`-times differentiable in an open interval between `x₀` and `x` (exclusive), and another function `g` is differentiable in this open interval and continuous in the closed interval, then there exists some `x'` within the open interval such that the difference between the function value at `x` and the Taylor polynomial of `f` of degree `n` evaluated between `x₀` and `x` equals the fraction of `n`-th power of the difference between `x` and `x'` and `n!` multiplied by the difference between the function values of `g` at `x` and `x₀` divided by the derivative of `g` at `x'`, scaled by the `(n+1)`-th derivative of `f` at `x'` within the closed interval. This theorem provides an estimate of the error made by approximating a function by its Taylor polynomial of degree `n`.
More concisely: If a `C^(n+1)` function `f` and a `C^1` function `g` are given on a closed interval [x₀, x], then for some `x'` in the open interval (x₀, x), the difference between `f(x)` and the `n`-th degree Taylor polynomial of `f` at `x₀` is equal to `(x - x')^n * (n!) ^-1 * g'(x') * f^((n+1))(x')`.
|
exists_taylor_mean_remainder_bound
theorem exists_taylor_mean_remainder_bound :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {n : ℕ},
a ≤ b →
ContDiffOn ℝ (↑n + 1) f (Set.Icc a b) →
∃ C, ∀ x ∈ Set.Icc a b, ‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
**Taylor's Theorem with Polynomial Bound on the Remainder**
Assume we have a function `f` that is continuously differentiable `n+1` times on the closed interval from `a` to `b` (denoted as `Icc a b` in Lean). This theorem states that there exists a constant `C` such that, for all `x` in the closed interval `Icc a b`, the difference between the function `f` at `x` and its Taylor polynomial of degree `n` can be bounded by `C * (x - a)^(n+1)`. In other words, we have an estimate for the error in using the `n`-th Taylor polynomial to approximate the function `f`.
More concisely: Given a continuously differentiable function `f` of order `n+1` on the closed interval `[a, b]`, there exists a constant `C` such that for all `x` in `[a, b]`, |`f(x) - Taylor.poly n a (x)`| ≤ `C * (x - a)^(n+1)`, where `Taylor.poly n a (x)` is the Taylor polynomial of degree `n` for `f` at `x = a`.
|
continuousOn_taylorWithinEval
theorem continuousOn_taylorWithinEval :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x : ℝ} {n : ℕ} {s : Set ℝ},
UniqueDiffOn ℝ s → ContDiffOn ℝ (↑n) f s → ContinuousOn (fun t => taylorWithinEval f n s t x) s
This theorem, `continuousOn_taylorWithinEval`, states that if a function `f` is `n` times continuously differentiable on a set `s` of real numbers, then the Taylor polynomial of `f` of degree `n`, evaluated within the set `s` at a point `x₀`, is continuous at `x₀`. In the context of this theorem, 'continuous' means that for every point `t` in `s`, the limit of the Taylor polynomial as `t` approaches `x₀` exists and equals the value of the Taylor polynomial at `x₀`. This holds for any normed additive commutative group `E` over the real numbers, given that `s` is a unique differential on `ℝ`.
More concisely: If a real-valued function `f` that is `n` times continuously differentiable on a set `s` has its Taylor polynomial of degree `n` evaluated at `x₀` in `s`, then the Taylor polynomial is continuous at `x₀`.
|
hasDerivWithinAt_taylorWithinEval_at_Icc
theorem hasDerivWithinAt_taylorWithinEval_at_Icc :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ},
a < b →
t ∈ Set.Icc a b →
ContDiffOn ℝ (↑n) f (Set.Icc a b) →
DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Icc a b) →
HasDerivWithinAt (fun y => taylorWithinEval f n (Set.Icc a b) y x)
(((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) (Set.Icc a b) t
This theorem states that for a given function `f` mapping real numbers to a normed space `E`, a real number `t` within a closed interval `[a, b]`, and a non-negative integer `n`, if `f` is continuously differentiable `n` times on the interval `[a, b]` and its `n`-th derivative is also differentiable on this interval, then the derivative of the Taylor polynomial of `f` of order `n` with respect to `t` exists and is equal to `(((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t`. This derivative is taken within the interval `[a, b]`.
More concisely: For a continuously differentiable function `f` of order `n+1` with an `n`-th derivative that is also differentiable on a closed interval `[a, b]`, the derivative of the `n`-th order Taylor polynomial of `f` at `t` within `[a, b]` equals `(1/(n!)*(x-t)^n*(f^(n+1))(t)`) where `x` is in `[a, b]`.
|
taylor_mean_remainder_cauchy
theorem taylor_mean_remainder_cauchy :
∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
x₀ < x →
ContDiffOn ℝ (↑n) f (Set.Icc x₀ x) →
DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x) →
∃ x' ∈ Set.Ioo x₀ x,
f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x =
iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / ↑n.factorial * (x - x₀)
The theorem is a statement of Taylor's theorem with the Cauchy form of the remainder. It states that, given a function `f` that is `n+1`-times continuously differentiable on the closed interval from `x₀` to `x`, and `n+1`-times differentiable on the open interval from `x₀` to `x`, there exists a point `x'` in the open interval from `x₀` to `x` such that the difference between the value of `f` at `x` and the value of the Taylor polynomial of `f` of degree `n` evaluated at `x₀` and `x` equals the `n+1`-th iterated derivative of `f` at `x'` times `(x - x')` to the power `n` divided by `n` factorial, all times `(x - x₀)`. Here, the Taylor polynomial of `f` is calculated with derivatives inside the closed interval from `x₀` to `x`.
More concisely: Given a function `f` that is `n+1`-times differentiable on the open interval between `x₀` and `x`, and `n+1`-times continuously differentiable on the closed interval between `x₀` and `x`, there exists `x'` in the open interval between `x₀` and `x` such that $f(x) = \sum\_{i=0}^n \frac{f^{(i)}(x\_0)}{i!}(x - x\_0)^i + \frac{f^{(n+1)}(x')}{(n+1)!}(x - x\_0)^{n+1}$.
|
taylor_mean_remainder_bound
theorem taylor_mean_remainder_bound :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C x : ℝ} {n : ℕ},
a ≤ b →
ContDiffOn ℝ (↑n + 1) f (Set.Icc a b) →
x ∈ Set.Icc a b →
(∀ y ∈ Set.Icc a b, ‖iteratedDerivWithin (n + 1) f (Set.Icc a b) y‖ ≤ C) →
‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n.factorial
**Taylor's Theorem with Remainder Bound**
This theorem is a version of Taylor's theorem that includes a bound for the remainder. It states that for any function `f` from `ℝ` to `E`, where `E` is a normed add commutative group with a normed space over `ℝ`, given a closed interval from `a` to `b`, a real number `C`, another real number `x`, and a natural number `n`, if `f` is `n+1`-times continuously differentiable on the interval and `x` lies within the interval, and also the `n+1`-th iterated derivative of `f` is bounded by `C` on the interval, then the difference between `f(x)` and the `n`-th Taylor polynomial of `f` at `x`, evaluated at `a`, is bounded by `C * (x - a)^(n+1) / n!`. The main takeaway is that the error between the function and its Taylor polynomial can be bounded by a term involving the `(n+1)`-th derivative.
More concisely: Given a function `f` that is `n+1`-times continuously differentiable on a closed interval [a, b] with bounded `(n+1)$-th derivative, the error between `f(x)` and the `n`-th Taylor polynomial of `f` at `x` evaluated at `a` is bounded by `C * |x - a|^(n+1) / n!`.
|
taylorWithinEval_hasDerivAt_Ioo
theorem taylorWithinEval_hasDerivAt_Ioo :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ},
a < b →
t ∈ Set.Ioo a b →
ContDiffOn ℝ (↑n) f (Set.Icc a b) →
DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Ioo a b) →
HasDerivAt (fun y => taylorWithinEval f n (Set.Icc a b) y x)
(((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) t
This theorem, `taylorWithinEval_hasDerivAt_Ioo`, states that for any real-valued function `f`, a real number `t` in the open interval `(a, b)`, and a natural number `n`, if the function `f` is `n` times continuously differentiable on the closed interval `[a, b]` and the `n`-th iterated derivative of `f` exists on the open interval `(a, b)`, then the derivative at `t` of the Taylor polynomial of order `n` for `f` evaluated at `x` exists and is equal to `((n.factorial)⁻¹ * (x - t) ^ n) * (n + 1)`-th iterated derivative of `f` at `t`. In mathematical notation, it says that if $f$ is $n$ times differentiable on $[a, b]$ and its $n$-th derivative exists on $(a, b)$, then $\frac{d}{dt} P_n(t, x) = ((n!)^{-1} * (x - t) ^ n) * f^{(n+1)}(t)$, where $P_n(t, x)$ is the Taylor polynomial of order $n$ for $f$ evaluated at $x$.
More concisely: Given a real-valued function `f` that is `n` times continuously differentiable on `[a, b]` with the `n`-th derivative existing on `(a, b)`, the derivative of the `n`-th order Taylor polynomial of `f` evaluated at `x` is equal to `((n!)^(-1) * (x - t)^n * f^{(n+1)}(t))`.
|
taylorWithinEval_self
theorem taylorWithinEval_self :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ),
taylorWithinEval f n s x₀ x₀ = f x₀
This theorem states that for any normed additive commutative group `E` over the real numbers `ℝ`, any function `f` from `ℝ` to `E`, any natural number `n`, any set `s` of real numbers, and any real number `x₀`, if we evaluate the Taylor polynomial of `f` up to degree `n`, computed within the set `s` and centered at `x₀`, at `x₀`, it will yield the value of the function `f` at `x₀`. In mathematical terms, it captures the idea that a Taylor polynomial provides an approximation to a function at a point, and the approximation is exact at the center of the series expansion.
More concisely: For any normed additive commutative group `E` over `ℝ`, any real-valued function `f` on `ℝ`, any natural number `n`, any set `s` of real numbers, and any real number `x₀`, the value of the Taylor polynomial of degree `n` of `f` centered at `x₀` is equal to `f` evaluated at `x₀`.
|
taylor_within_zero_eval
theorem taylor_within_zero_eval :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (s : Set ℝ) (x₀ x : ℝ),
taylorWithinEval f 0 s x₀ x = f x₀
This theorem states that for any real-valued function `f`, any set `s` of real numbers, and any two real numbers `x₀` and `x`, the evaluation of the Taylor polynomial of order zero, within the set `s`, at the point `x` equals the value of the function `f` at the point `x₀`. In other words, the zeroth-order Taylor approximation of a function `f` at a point `x₀` within a set `s` is simply the value of the function at `x₀`.
More concisely: For any real-valued function `f`, and for any set `s` of real numbers containing `x₀` and `x`, the zeroth-order Taylor polynomial of `f` at `x₀` equals `f x₀` within `s`.
|
taylor_mean_remainder_lagrange
theorem taylor_mean_remainder_lagrange :
∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
x₀ < x →
ContDiffOn ℝ (↑n) f (Set.Icc x₀ x) →
DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x) →
∃ x' ∈ Set.Ioo x₀ x,
f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x =
iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial
This is a statement of **Taylor's theorem** with the Lagrange form of the remainder. Given a function `f` that maps real numbers to real numbers, and two real numbers `x₀` and `x` where `x₀` is less than `x`, and a natural number `n`. If `f` is `n+1`-times continuously differentiable on the closed interval from `x₀` to `x` and `n+1`-times differentiable on the open interval from `x₀` to `x`, then the theorem asserts the existence of a real number `x'` in the open interval from `x₀` to `x` such that the difference between the value of `f` at `x` and the value of the `n`-th Taylor polynomial of `f` evaluated at `x₀` and `x` equals the `(n+1)`-th iterated derivative of `f` at `x'` times `(x - x₀)` to the power of `(n+1)` divided by the factorial of `(n+1)`. The `n`-th Taylor polynomial is computed with derivatives within the closed interval from `x₀` to `x`.
More concisely: Given a real-valued function `f` that is (n+1) times continuously differentiable on the closed interval [x₀, x] and (n+1) times differentiable on the open interval (x₀, x), there exists a real number x' in (x₀, x) such that f(x) = Pn(x₀, x) + (1/n!)(f^((n+1))(x'))*(x - x₀)^(n+1), where Pn is the n-th Taylor polynomial of f evaluated at x₀ and x.
|