ContDiffOn.differentiableOn_iteratedDerivWithin
theorem ContDiffOn.differentiableOn_iteratedDerivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} {m : β},
ContDiffOn π n f s β βm < n β UniqueDiffOn π s β DifferentiableOn π (iteratedDerivWithin m f s) s
This theorem states that for a function `f` from `π` to `F` that is continuously differentiable up to order `n` on a set `s`, if the derivatives up to order less than `n` are unique on `s` and `m` is less than `n`, then the `m`-th iterated derivative of `f` within `s` is differentiable on `s`. Here, `π` is a nontrivially normed field, `F` is a normed additive commutative group, and `s` is a set in `π`. This theorem thus expresses a key property of higher-order derivatives.
More concisely: If a continuously differentiable up to order `n` function `f` from a nontrivially normed field `π` to a normed additive commutative group `F` has unique derivatives up to order less than `n` on a set `s`, then the `m`-th iterated derivative of `f` is differentiable on `s` for `m < n`.
|
iteratedDerivWithin_succ'
theorem iteratedDerivWithin_succ' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π},
UniqueDiffOn π s β x β s β iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x
This theorem states that for a given function `f` mapping from a non-trivially normed field `π` to a normed add commutative group `F`, and a set `s` of elements from `π` where each point is distinct in terms of tangents (`UniqueDiffOn π s`), if a point `x` belongs to the set `s`, then the `(n+1)`-th iterated derivative of `f` within the set `s` at point `x` is equal to the `n`-th iterated derivative of the derivative of `f` within the set `s` at point `x`. In other words, the theorem asserts that we can stepwise compute the iterated derivative within a set by taking the derivative of the previous iterated derivative.
More concisely: For a function `f` from a non-trivially normed field to a normed add commutative group, and a set `s` of distinct points, if `x` is in `s` then the `(n+1)`-th derivative of `f` at `x` equals the `n`-th derivative of `f'` at `x`, where `f'` is the derivative of `f`.
|
iteratedDeriv_eq_equiv_comp
theorem iteratedDeriv_eq_equiv_comp :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F},
iteratedDeriv n f = β(ContinuousMultilinearMap.piFieldEquiv π (Fin n) F).symm β iteratedFDeriv π n f
The theorem `iteratedDeriv_eq_equiv_comp` states that for any nontrivially normed field `π`, a normed add commutative group `F`, and a normed space `F` over `π`, the `n`-th iterated derivative of a function `f` from `π` to `F` can be written as the composition of the inverse of a continuous linear equivalence and the `n`-th iterated FrΓ©chet derivative of `f`. More formally, given any natural number `n` and a function `f` from `π` to `F`, the `n`-th iterated derivative of `f` is equal to the composition of the inverse of the continuous multilinear map `piFieldEquiv` applied to `π`, `Fin n`, and `F`, and the `n`-th iterated FrΓ©chet derivative of `f`.
More concisely: For any nontrivially normed field `π`, add commutative group `F`, and normed space `F` over `π`, the `n`-th iterated derivative of a function `f` from `π` to `F` equals the composition of the inverse of the continuous linear equivalence `ΟFieldEquiv` and the `n`-th iterated Frechet derivative of `f`.
|
iteratedDerivWithin_zero
theorem iteratedDerivWithin_zero :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π}, iteratedDerivWithin 0 f s = f
The theorem `iteratedDerivWithin_zero` states that for any given non-trivial normed field `π`, any normed additive commutative group `F`, a normed space structure over `π` and `F`, a function `f` from `π` to `F`, and a set `s` of `π`, the zero-th iterated derivative of the function `f` within the set `s` is just the function `f` itself. In other words, applying the operation of taking the derivative zero times leaves any function unchanged.
More concisely: For any normed field π, normed additive commutative group F, normed space structure on F over π, function f from π to F, and set s of π, the zero-th iterated derivative of f within s equals f.
|
iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod
theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {x : π} {m : Fin n β π},
(iteratedFDeriv π n f x) m = (Finset.univ.prod fun i => m i) β’ iteratedDeriv n f x
The theorem `iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod` states that for any non-trivially normed field `π`, normed add commutative group `F`, normed space over `π` of `F`, natural number `n`, function `f` from `π` to `F`, element `x` of `π`, and function `m` from a finite set of `n` elements to `π`, the `n`-th FrΓ©chet derivative of `f` evaluated at `x` and applied to a vector `(m 0, ..., m (n-1))` is equal to the product of the `m i`s multiplied by the `n`-th iterated derivative of `f` evaluated at `x`. This theorem ties together the concepts of iterated FrΓ©chet and standard derivatives, showing how they relate to each other in the context of normed vector spaces.
More concisely: For any non-trivially normed field `π`, normed add commutative group `F`, normed space over `π` of `F`, natural number `n`, function `f` from `π` to `F`, element `x` of `π`, and function `m` from a finite set of `n` elements to `π`, the `n`-th FrΓ©chet derivative of `f` at `x` applied to `(m 0, ..., m (n-1))` equals the product of `m`'s values multiplied by the `n`-th iterated derivative of `f` at `x`.
|
iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod
theorem iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π} {m : Fin n β π},
(iteratedFDerivWithin π n f s x) m = (Finset.univ.prod fun i => m i) β’ iteratedDerivWithin n f s x
This theorem, named `iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod`, states that for any nontrivially normed field `π`, normed add commutative group `F`, and normed space over `π` and `F`, given a natural number `n`, a function `f` from `π` to `F`, a set `s` of elements of type `π`, an element `x` of type `π`, and a function `m` from the finite set of the first `n` natural numbers to `π`, the `n`-th FrΓ©chet derivative of `f` at `x` within `s` applied to the vector `(m 0, ..., m (n-1))` is equal to the scalar multiplication of the `n`-th iterated derivative of `f` at `x` within `s` by the product of the elements `m i` for all `i` in the finite set of the first `n` natural numbers. This essentially relates the FrΓ©chet derivative of a function to its iterated derivative while considering the multiplication of all elements in a given vector.
More concisely: For any nontrivially normed field `π`, normed add commutative group `F`, and normed space over `π` and `F`, the `n`-th FrΓ©chet derivative of a function `f` from `π` to `F` at `x` within `s` applied to the vector `(m 0, ..., m (n-1))` equals the scalar multiplication of the `n`-th iterated derivative of `f` at `x` within `s` by the product of `m i` for all `i` in the first `n` natural numbers.
|
iteratedDeriv_eq_iterate
theorem iteratedDeriv_eq_iterate :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F}, iteratedDeriv n f = deriv^[n] f
The theorem `iteratedDeriv_eq_iterate` states that for any function `f` from some non-trivially normed field `π` to a normed additive commutative group `F`, under the normed space structure of `π` and `F`, the `n`-th iterated derivative of `f` is equivalent to applying the differentiation operation `n` times to `f`. In other words, for any natural number `n`, the `n`-th iterated derivative of `f` is the same as the `n`-th power of the `deriv` function applied to `f`. This connects the concept of iterated derivatives with repeated differentiation.
More concisely: For any function `f` from a non-trivially normed field to a normed additive commutative group, the `n`-th iterated derivative of `f` equals the `n`-th power of the derivative function applied to `f`.
|
iteratedDeriv_succ'
theorem iteratedDeriv_succ' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F}, iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
The theorem `iteratedDeriv_succ'` states that for any type `π` with a non-trivially normed field structure, any type `F` with a normed additive commutative group structure and a normed space over `π` structure, any natural number `n`, and any function `f` from `π` to `F`, the `n+1`-th iterated derivative of `f` is equal to the `n`-th derivative of the derivative of `f`. In other words, taking the `n+1`-th derivative is the same as taking the derivative first, and then taking the `n`-th derivative of the result. This corresponds to the familiar rule from calculus that the `n+1`-th derivative of a function is obtained by taking the derivative of the `n`-th derivative.
More concisely: For any normed field `π`, normed additive commutative group `F` over `π`, natural number `n`, and function `f` from `π` to `F` with normed space over `π` structure, the `(n+1)`-th iterated derivative of `f` equals the `n`-th derivative of its derivative.
|
contDiffOn_of_continuousOn_differentiableOn_deriv
theorem contDiffOn_of_continuousOn_differentiableOn_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {n : ββ},
(β (m : β), βm β€ n β ContinuousOn (fun x => iteratedDerivWithin m f s x) s) β
(β (m : β), βm < n β DifferentiableOn π (fun x => iteratedDerivWithin m f s x) s) β ContDiffOn π n f s
This theorem states that if the first `n` derivatives within a set of a function are continuous, and its first `n-1` derivatives are differentiable, then the function is continuously differentiable up to order `n` - a property denoted as `C^n`. This is not generally an equivalence, but it becomes an equivalence when the set has unique derivatives. This is captured in the lemma `contDiffOn_iff_continuousOn_differentiableOn_deriv`. The theorem takes as parameters a base field `π` (which is assumed to be a non-trivially normed field), a target type `F` (which is assumed to be a normed additive commutative group and a normed space over `π`), a function `f` from `π` to `F`, a set `s` of type `Set π`, and a natural number `n` (denoting the order of continuity and differentiability).
More concisely: If a function from a non-trivially normed field to a normed additive commutative group and normed space is continuously differentiable up to order `n` on a set with unique derivatives, then its first `n` derivatives are continuous on that set.
|
contDiffOn_iff_continuousOn_differentiableOn_deriv
theorem contDiffOn_iff_continuousOn_differentiableOn_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {n : ββ},
UniqueDiffOn π s β
(ContDiffOn π n f s β
(β (m : β), βm β€ n β ContinuousOn (iteratedDerivWithin m f s) s) β§
β (m : β), βm < n β DifferentiableOn π (iteratedDerivWithin m f s) s)
This theorem states that for any function `f` from a non-trivially normed field `π` to a normed add commutative group `F`, a set `s` of `π`, and a natural number or infinity `n`, given that `s` has unique derivatives, the property of `f` being continuously differentiable `n` times on `s` is equivalent to both the property that the `m`-th iterated derivative of `f` on `s` is continuous on `s` for all `m` less than or equal to `n`, and the property that it is differentiable on `s` for all `m` less than `n`.
More concisely: A function `f` from a non-trivially normed field to a normed add commutative group is continuously differentiable `n` times on a set `s` if and only if all its iterated derivatives up to order `n` are continuous on `s` and the function is differentiable on `s` for orders less than `n`.
|
iteratedDerivWithin_eq_equiv_comp
theorem iteratedDerivWithin_eq_equiv_comp :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π},
iteratedDerivWithin n f s =
β(ContinuousMultilinearMap.piFieldEquiv π (Fin n) F).symm β iteratedFDerivWithin π n f s
This theorem states that for any non-trivially normed field `π`, normed add commutative group `F`, natural number `n`, function `f` from `π` to `F`, and a set `s` of `π`, the `n`-th iterated derivative of `f` within `s` can be expressed as the composition of the inverse of a continuous multilinear map from `π^n` to `F` and the `n`-th iterated FrΓ©chet derivative of `f` within `s`. In other words, it elucidates a connection between the conventional iterated derivative and the iterated FrΓ©chet derivative in the context of continuous linear maps.
More concisely: For any non-trivially normed field `π`, normed additive group `F`, natural number `n`, function `f` from `π` to `F`, and set `s` in `π`, the `n`-th iterated derivative of `f` on `s` equals the composition of the inverse of the `n`-th iterated Frechet derivative of `f` on `s` and the `n`-th iterated Frechet derivative of `f` on `s`.
|
contDiff_iff_iteratedDeriv
theorem contDiff_iff_iteratedDeriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {n : ββ},
ContDiff π n f β
(β (m : β), βm β€ n β Continuous (iteratedDeriv m f)) β§
β (m : β), βm < n β Differentiable π (iteratedDeriv m f)
The theorem `contDiff_iff_iteratedDeriv` states that for any function `f` from a nontrivially normed field `π` to a normed add commutative group `F`, under the normed space structure, and for any `n` in extended natural numbers (i.e., the set of natural numbers union infinity), the function `f` is continuously differentiable up to order `n` if and only if two conditions are met:
1. For every natural number `m` less than or equal to `n`, the `m`-th iterated derivative of `f` is a continuous function.
2. For every natural number `m` strictly less than `n`, the `m`-th iterated derivative of `f` is differentiable at every point.
In other words, the property of being continuously differentiable up to order `n` can be reformulated in terms of conditions involving the iterated one-dimensional derivative.
More concisely: A function from a nontrivially normed field to a normed add commutative group is continuously differentiable up to order n if and only if all its iterated derivatives of order less than n are continuous and differentiable at every point.
|
contDiff_of_differentiable_iteratedDeriv
theorem contDiff_of_differentiable_iteratedDeriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {n : ββ},
(β (m : β), βm β€ n β Differentiable π (iteratedDeriv m f)) β ContDiff π n f
The theorem `contDiff_of_differentiable_iteratedDeriv` states that, for a function `f` from a non-trivially normed field `π` to a normed additive commutative group `F`, if all of its first `n` derivatives are differentiable, then the function `f` is `n` times continuously differentiable. This statement is a bit stronger than necessary because it requires the `n`-th derivative to be differentiable rather than just continuous, but this condition simplifies the proof and is optimal when `n` tends to infinity.
More concisely: If a function `f` from a non-trivially normed field to a normed additive commutative group has all its first `n` derivatives differentiable, then `f` is `n`-times continuously differentiable.
|
iteratedFDerivWithin_eq_equiv_comp
theorem iteratedFDerivWithin_eq_equiv_comp :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π},
iteratedFDerivWithin π n f s = β(ContinuousMultilinearMap.piFieldEquiv π (Fin n) F) β iteratedDerivWithin n f s
This theorem states that for any non-trivial normed field `π`, normed additive commutative group `F`, natural number `n`, function `f` from `π` to `F`, and set `s` of `π`, the `n`-th iterated FrΓ©chet derivative of `f` within `s` is equivalent to the composition of the continuous linear equiv (given by `ContinuousMultilinearMap.piFieldEquiv π (Fin n) F`) and the `n`-th iterated derivative of `f` within `s`. In other words, we can obtain the `n`-th iterated FrΓ©chet derivative by first applying the `n`-th iterated derivative and then applying the continuous linear equiv.
More concisely: For any non-trivial normed field `π`, normed additive commutative group `F`, natural number `n`, function `f` from `π` to `F`, and set `s` of `π`, the `n`-th iterated FrΓ©chet derivative of `f` within `s` is equal to the composition of the continuous linear equiv `ContinuousMultilinearMap.piFieldEquiv π (Fin n) F` and the `n`-th iterated derivative of `f` within `s`.
|
contDiffOn_of_differentiableOn_deriv
theorem contDiffOn_of_differentiableOn_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {n : ββ},
(β (m : β), βm β€ n β DifferentiableOn π (iteratedDerivWithin m f s) s) β ContDiffOn π n f s
This theorem states that in order to verify that a function `f` from a type `π` to a type `F` is `n` times continuously differentiable on a set `s` of type `π`, it suffices to confirm that its first `n` derivatives are differentiable on `s`. The derivatives are taken as per the `iteratedDerivWithin` function, meaning they are iteratively calculated within the set `s`. The theorem's statement leans towards being a bit stronger than needed, as it requires differentiability of the `n`-th derivative rather than its continuity. However, this approach simplifies the proof by excluding the continuity discussion, and it's optimal when `n` is infinity.
More concisely: To verify that a function `f` from a type `π` to a type `F` is `n`-times differentiable on a set `s` of type `π`, it is sufficient to show that its first `n` derivatives are differentiable within `s`.
|
iteratedDerivWithin_succ
theorem iteratedDerivWithin_succ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π},
UniqueDiffWithinAt π s x β iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
The theorem `iteratedDerivWithin_succ` states that for a given nontrivially normed field `π`, a normed additive commutative group `F`, a normed space `π F`, a natural number `n`, a function `f` from `π` to `F`, a set `s` of `π`, and an element `x` of `π`, if the set `s` has unique derivatives at the point `x`, then the `(n+1)`-th iterated derivative of the function `f` within the set `s` at the point `x` can be obtained by finding the derivative within the set `s` at the point `x` of the `n`-th iterated derivative of the function `f` within the set `s`. In mathematical terms, if `f : π β F` is differentiable within a set `s` at a point `x`, then the `(n+1)`-th derivative at `x` within `s` of `f`, denoted `iteratedDerivWithin (n + 1) f s x`, is equal to the derivative at `x` within `s` of the `n`-th derivative of `f`, denoted `derivWithin (iteratedDerivWithin n f s) s x`.
More concisely: If a function `f : π β F` is `n`-times differentiable within a set `s` at a point `x` in a nontrivially normed field `π`, then the `(n+1)`-th derivative of `f` within `s` at `x` is equal to the derivative of the `n`-th derivative of `f` within `s` at `x`.
|
ContDiffOn.continuousOn_iteratedDerivWithin
theorem ContDiffOn.continuousOn_iteratedDerivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {f : π β F} {s : Set π} {n : ββ} {m : β},
ContDiffOn π n f s β βm β€ n β UniqueDiffOn π s β ContinuousOn (iteratedDerivWithin m f s) s
This theorem states that, for any nontrivial normed field `π`, normed additive commutative group `F`, and function `f` from `π` to `F`, as well as any set `s` of `π` and natural numbers `n` and `m` (with `m` less than or equal to `n`), if `f` is `C^n` continuous differentiable on `s` and `s` has unique derivatives, then the `m`-th iterated derivative of `f` within `s` is continuous on `s`. In plain language, on a set where each point has a unique tangent line, a function that is continuously differentiable up to a certain order has all its derivatives up to that order being continuous.
More concisely: If `f` is a `C^n` differentiable function with unique derivatives on a nontrivial normed field `π` and normed additive commutative group `F`, then the `m`-th iterated derivative of `f` is continuous on `π` for all `m` with `0 β€ m β€ n`.
|
iteratedFDeriv_eq_equiv_comp
theorem iteratedFDeriv_eq_equiv_comp :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F},
iteratedFDeriv π n f = β(ContinuousMultilinearMap.piFieldEquiv π (Fin n) F) β iteratedDeriv n f
The theorem `iteratedFDeriv_eq_equiv_comp` states that for any nontrivially normed field `π`, normed additive commutative group `F`, and a function `f` from `π` to `F`, the `n`-th iterated FrΓ©chet derivative of `f` is equivalent to the composition of a continuous multilinear map from the field `π` to `F` and the `n`-th iterated derivative of `f`. In other words, it asserts that the `n`-th iterated FrΓ©chet derivative can be expressed as the `n`-th iterated derivative followed by a certain continuous linear transformation.
More concisely: For any nontrivially normed field π, normed additive commutative group F, and function f from π to F, the n-th iterated FrΓ©chet derivative of f is equivalent to the composition of the n-th iterated derivative of f with a continuous multilinear map from π to F.
|
iteratedDeriv_succ
theorem iteratedDeriv_succ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F}, iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)
The theorem `iteratedDeriv_succ` states that for any nontrivial normed field `π`, normed additive commutative group `F`, and a function `f` from `π` to `F`, the `n+1`-th iterated derivative of `f` can be obtained by differentiating the `n`-th iterated derivative of `f`. In other words, if we denote the `n`-th iterated derivative of `f` as `f^(n)`, then the `n+1`-th iterated derivative `f^(n+1)` is the derivative of `f^(n)`.
More concisely: For any normed field π, normed additive commutative group F, and differentiable function f from π to F, the n-th iterated derivative of f is the derivative of the n-th iterated derivative of f, i.e., (d/dx)(f^n(x)) = f^(n+1)(x).
|
iteratedDerivWithin_eq_iterate
theorem iteratedDerivWithin_eq_iterate :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : β} {f : π β F} {s : Set π} {x : π},
UniqueDiffOn π s β x β s β iteratedDerivWithin n f s x = (fun g => derivWithin g s)^[n] f x
The theorem `iteratedDerivWithin_eq_iterate` states that, given a non-trivially normed field `π`, a normed additive commutative group `F`, a function `f` from `π` to `F`, a natural number `n`, a set `s` of `π`, and an element `x` in `π`, if `s` is uniquely differentiable (`UniqueDiffOn π s`) and `x` is a member of `s`, then the `n`-th iterated derivative of `f` within the set `s` at the point `x` (`iteratedDerivWithin n f s x`) is equal to the result of applying the derivative function within the set `s` `n` times to the function `f` at the point `x` (`(fun g => derivWithin g s)^[n] f x`). This highlights that the `n`-th iterated derivative within a set with unique derivatives can be computed by repeatedly applying the differentiation operation `n` times.
More concisely: For a non-trivially normed field `π`, a normed additive commutative group `F`, a uniquely differentiable function `f` from `π` to `F`, a natural number `n`, a set `s` of `π` containing a point `x` in `π`, the `n`-th iterated derivative of `f` within `s` at `x` equals the `n`-fold composition of the derivative function within `s` with `f` at `x`.
|