norm_iteratedFDerivWithin_comp_le_aux
theorem norm_iteratedFDerivWithin_comp_le_aux :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {Fu Gu : Type u} [inst_3 : NormedAddCommGroup Fu] [inst_4 : NormedSpace ๐ Fu]
[inst_5 : NormedAddCommGroup Gu] [inst_6 : NormedSpace ๐ Gu] {g : Fu โ Gu} {f : E โ Fu} {n : โ} {s : Set E}
{t : Set Fu} {x : E},
ContDiffOn ๐ (โn) g t โ
ContDiffOn ๐ (โn) f s โ
UniqueDiffOn ๐ t โ
UniqueDiffOn ๐ s โ
Set.MapsTo f s t โ
x โ s โ
โ {C D : โ},
(โ i โค n, โiteratedFDerivWithin ๐ i g t (f x)โ โค C) โ
(โ (i : โ), 1 โค i โ i โค n โ โiteratedFDerivWithin ๐ i f s xโ โค D ^ i) โ
โiteratedFDerivWithin ๐ n (g โ f) s xโ โค โn.factorial * C * D ^ n
This theorem states that: given two functions `g` and `f` mapping from normed spaces `Fu` and `E` to `Gu` and `Fu` respectively, and a natural number `n`, if the `n`-th continuous derivatives of `g` on set `t` and `f` on set `s` exist, and the sets `s` and `t` are uniquely differentiable, with `f` mapping `s` into `t`, and a point `x` belongs to `s`; then for any real numbers `C` and `D`, if the derivatives up to `n` of `g` at `f(x)` are bounded by `C`, and derivatives up to `n` of `f` at `x` are bounded by `D` raised to the power of the derivative's order; then the `n`-th derivative of the composition `g โ f` at `x` is bounded by `n! (n factorial) * C * D^n`. This theorem is a version of the result that assumes two of the normed spaces are in the same universe, which allows for induction in its proof. A more general version of the theorem is given by `norm_iteratedFDerivWithin_comp_le`, which doesn't require this assumption.
More concisely: Given functions `g: Fu -> Gu` and `f: E -> Fu` between normed spaces, if the `n`-th derivatives of `g` and `f` exist and are bounded on uniquely differentiable sets `s` and `t` with `f(s) = t`, and the derivatives of `f` at a point `x` in `s` are bounded by some power of the derivative's order `D`, and the derivatives of `g` at `f(x)` are bounded by `C`, then the `n`-th derivative of `g โ f` at `x` is bounded by `n! * C * D^n`.
|
norm_iteratedFDerivWithin_comp_le
theorem norm_iteratedFDerivWithin_comp_le :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ๐ F] {G : Type uG}
[inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ๐ G] {g : F โ G} {f : E โ F} {n : โ} {s : Set E} {t : Set F}
{x : E} {N : โโ},
ContDiffOn ๐ N g t โ
ContDiffOn ๐ N f s โ
โn โค N โ
UniqueDiffOn ๐ t โ
UniqueDiffOn ๐ s โ
Set.MapsTo f s t โ
x โ s โ
โ {C D : โ},
(โ i โค n, โiteratedFDerivWithin ๐ i g t (f x)โ โค C) โ
(โ (i : โ), 1 โค i โ i โค n โ โiteratedFDerivWithin ๐ i f s xโ โค D ^ i) โ
โiteratedFDerivWithin ๐ n (g โ f) s xโ โค โn.factorial * C * D ^ n
The theorem `norm_iteratedFDerivWithin_comp_le` states that, given a non-trivially normed field `๐` and normed add commutative groups `E`, `F`, and `G` with their respective normed spaces. If we have two functions `g : F โ G` and `f : E โ F`, a natural number `n`, and two sets `s : Set E` and `t : Set F` with `x` being an element of `s`, and a natural number or infinity `N`. If `g` is continuously differentiable on `t` and `f` is continuously differentiable on `s` up to order `N`, `n` is less than or equal to `N`, `t` and `s` have unique differentiability and `f` maps each point in `s` to a point in `t`. Suppose that the derivatives (up to `n`) of `g` at `f x` are bounded by a real number `C`, and the `i`-th derivative of `f` at `x` is bounded by `D^i` for each `i` from `1` to `n`. Then the `n`-th derivative of the composition `g โ f` at `x` is bounded by the factorial of `n` times `C` times `D` to the power `n`.
More concisely: Given a non-trivially normed field and normed add commutative groups with continuously differentiable functions `g : F โ G` and `f : E โ F`, if `g` is `N`-times differentiable with bounded derivatives, `f` is `N`-times differentiable at `x` with bounded derivatives, and `g(fx)` has `n`-th derivative bounded by the factorial of `n` times the product of `C` and `D^n`, then the `n`-th derivative of `g โ f` at `x` exists and is also bounded by the same value.
|
norm_iteratedFDeriv_comp_le
theorem norm_iteratedFDeriv_comp_le :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace ๐ E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ๐ F] {G : Type uG}
[inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ๐ G] {g : F โ G} {f : E โ F} {n : โ} {N : โโ},
ContDiff ๐ N g โ
ContDiff ๐ N f โ
โn โค N โ
โ (x : E) {C D : โ},
(โ i โค n, โiteratedFDeriv ๐ i g (f x)โ โค C) โ
(โ (i : โ), 1 โค i โ i โค n โ โiteratedFDeriv ๐ i f xโ โค D ^ i) โ
โiteratedFDeriv ๐ n (g โ f) xโ โค โn.factorial * C * D ^ n
This theorem states that if `g` and `f` are functions whose derivatives at a point `x` are bounded by constants `C` and `D` respectively, then the `n-th` derivative of the composition of `g` and `f` at `x` is bounded by the product of `n` factorial, `C`, and `D` raised to the `n-th` power. More specifically, the derivatives of `g` at `f(x)` are bounded by `C`, and the `i-th` derivative of `f` at `x` is bounded by `D` to the power of `i` for all `i` such that `1 โค i โค n`.
More concisely: If functions `f` and `g` have derivative bounds `C` and `D` at point `x`, respectively, then the `n`-th derivative of `g โ f` at `x` is bounded by `n! * C * D^n`.
|