iteratedFDerivWithin_add_apply
theorem iteratedFDerivWithin_add_apply :
β {π : 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] {s : Set E}
{x : E} {i : β} {f g : E β F},
ContDiffOn π (βi) f s β
ContDiffOn π (βi) g s β
UniqueDiffOn π s β
x β s β
iteratedFDerivWithin π i (f + g) s x = iteratedFDerivWithin π i f s x + iteratedFDerivWithin π i g s x
The theorem `iteratedFDerivWithin_add_apply` states that, given a non-trivially normed field `π`, and normed additive commutative groups `E` and `F` which are also normed `π`-spaces, a set `s` of elements of `E`, an element `x` of `E`, an integer `i`, and two functions `f` and `g` from `E` to `F`, if `f` and `g` are `i`-times continuously differentiable on `s`, `s` admits a unique differential at every point, and `x` is an element of `s`, then the `i`-th derivative of the sum of `f` and `g` at `x`, taken within the set `s`, is equal to the sum of the `i`-th derivatives of `f` and `g` at `x`, each taken within the set `s`. This is essentially a generalization of the rule of derivatives which states that the derivative of the sum of two functions is the sum of the derivatives.
More concisely: Given a non-trivially normed field `π`, normed additive commutative groups `E` and `F` that are also `π`-spaces, if `f` and `g` are `i`-times differentiable functions from `E` to `F` over a set `s` where `s` admits unique differentials at every point and contains `x`, then the `i`-th derivative of `f + g` at `x` equals the sum of the `i`-th derivatives of `f` and `g` at `x` within `s`.
|
ContDiffAt.fderiv
theorem ContDiffAt.fderiv :
β {π : 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] {xβ : E} {m : ββ} {f : E β F β G} {g : E β F} {n : ββ},
ContDiffAt π n (Function.uncurry f) (xβ, g xβ) β
ContDiffAt π m g xβ β m + 1 β€ n β ContDiffAt π m (fun x => fderiv π (f x) (g x)) xβ
The theorem `ContDiffAt.fderiv` states that if the function `f : E β F β G`, which is uncurried to `(E, F) β G`, is continuously differentiable at the point `(xβ, g xβ)` of order `n`, and another function `g : E β F` is continuously differentiable at the point `xβ` of order `m`, then the function `x β¦ fderiv π (f x) (g x)`, which maps an input `x` to the derivative of `f(x)` at `g(x)`, is also continuously differentiable at `xβ` of order `m`, provided that `m + 1` is less than or equal to `n`. Here, `π` is a non-trivial normed field and `E, F, G` are normed vector spaces over `π`. The orders of differentiability `m` and `n` can be any extended natural number (including infinity).
More concisely: If functions `f : E -> F -> G` and `g : E -> F` are continuously differentiable at points `(xβ, g(xβ))` and `xβ`, respectively, with orders `n` and `m`, respectively, then the composite function `x mapsto fderivββ‘(x)(g(x))` is continuously differentiable at `xβ` of order `min(m, n - 1)`.
|
ContDiff.snd'
theorem ContDiff.snd' :
β {π : 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] {n : ββ} {f : F β G},
ContDiff π n f β ContDiff π n fun x => f x.2
This theorem, `ContDiff.snd'`, states that for any non-trivially normed field `π`, normed add commutative groups `E`, `F`, and `G`, and any `C^n` function `f` from `F` to `G`, precomposing `f` with `Prod.snd` results in another `C^n` function. In other words, if `f` is `n` times continuously differentiable, then the function that applies `f` to the second element of a pair is also `n` times continuously differentiable.
More concisely: If `f` is a `C^n` function from a normed add commutative group `F` to another normed add commutative group `G` over a non-trivially normed field `π`, then `Prod.snd β f` is also a `C^n` function.
|
ContinuousLinearMap.iteratedFDeriv_comp_right
theorem ContinuousLinearMap.iteratedFDeriv_comp_right :
β {π : 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] {n : ββ} (g : G βL[π] E) {f : E β F},
ContDiff π n f β
β (x : G) {i : β},
βi β€ n β iteratedFDeriv π i (f β βg) x = (iteratedFDeriv π i f (g x)).compContinuousLinearMap fun x => g
The theorem `ContinuousLinearMap.iteratedFDeriv_comp_right` states that for any nontrivial normed field `π`, normed add commutative groups `E`, `F`, and `G` that are also normed spaces over `π`, a continuous linear map `g : G βL[π] E`, a function `f : E β F` which is `n`-times continuously differentiable, and any natural number `i` less than or equal to `n`, the `i`-th iterated FrΓ©chet derivative of the composite function `f β βg` equals the `i`-th iterated FrΓ©chet derivative of `f` composed with the linear map `g`. This basically tells us how to differentiate a function after it has been composed with a continuous linear map.
More concisely: For any nontrivial normed field π, normed add commutative groups/normed spaces E, F, and G, a continuously linear map g : G ββ E, an n-times differentiable function f : E β F, and any natural i < n, the i-th iterated FrΓ©chet derivative of f β g equals the composition of the i-th iterated FrΓ©chet derivative of f with g.
|
contDiff_add
theorem contDiff_add :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : ββ}, ContDiff π n fun p => p.1 + p.2
The theorem `contDiff_add` asserts that for any nontrivially normed field `π` and any normed additive commutative group `F` that is also a normed space over `π`, the addition operation is continuously differentiable of any order `n`. In simpler terms, it means that the function which adds together two elements of the vector space `F` has derivatives of all orders, and these derivatives are continuous functions.
More concisely: For any nontrivially normed field `π` and normed additive commutative group `F` that is also a normed space over `π`, the addition function `F Γ F β F` is continuously differentiable of all orders.
|
ContDiff.comp
theorem ContDiff.comp :
β {π : 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] {n : ββ} {g : F β G} {f : E β F},
ContDiff π n g β ContDiff π n f β ContDiff π n (g β f)
This theorem states that if we have two functions, `f` and `g`, where `f` maps from a normed additively commutative group `E` to `F` and `g` maps from `F` to `G`, all over a nontrivially normed field `π`, then the composition of these functions `g β f` is continuously differentiable up to the `n`th derivative if both `f` and `g` are also continuously differentiable up to the `n`th derivative. This is true for all `n` in the extended natural numbers `ββ`, which includes infinity.
More concisely: If `f : E β F` and `g : F β G` are `n`-times continuously differentiable functions between normed spaces over a nontrivially normed field, then their composition `g β f` is also `n`-times continuously differentiable.
|
contDiff_smul
theorem contDiff_smul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : ββ}, ContDiff π n fun p => p.1 β’ p.2
This theorem states that for any nontrivially normed field `π` and any normed additive commutative group `F` which is also a normed space over `π`, and for any natural number `n` (possibly infinity), the function that maps a pair `(π, F)` to the scalar multiplication of the pair, i.e., `p.1 β’ p.2`, is `n`-times continuously differentiable. This implies that scalar multiplication is a smooth operation in this context.
More concisely: For any nontrivially normed field `π` and normed additive commutative group `F` over `π` that is also a normed space, the scalar multiplication function `(π, F) β¦ π β’ F` is `n`-times continuously differentiable.
|
HasFTaylorSeriesUpToOn.continuousLinearMap_comp
theorem HasFTaylorSeriesUpToOn.continuousLinearMap_comp :
β {π : 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] {s : Set E} {f : E β F} {n : ββ}
{p : E β FormalMultilinearSeries π E F} (g : F βL[π] G),
HasFTaylorSeriesUpToOn n f p s β
HasFTaylorSeriesUpToOn n (βg β f) (fun x k => g.compContinuousMultilinearMap (p x k)) s
The theorem states that for any non-trivial normed field `π`, and any normed additive commutative groups `E`, `F`, and `G` which are also normed spaces over `π`, if a function `f` from `E` to `F` admits a Taylor series `p` within a set `s` of `E`, and if `g` is a linear map from `F` to `G`, then the composition of `g` and `f`, denoted as `g β f`, also admits a Taylor series within the same set `s`. The `k`-th term of this new Taylor series is given by the composition of `g` and the `k`-th term of the original Taylor series `p`.
More concisely: If `f: E β F` is a function with Taylor series `p` on a set `s` in a normed field `π`, and `g: F β G` is a linear map, then `g β f` has a Taylor series `q` on `s` with `q_(k) = g(p_(k))`.
|
ContDiffWithinAt.fderivWithin_right
theorem ContDiffWithinAt.fderivWithin_right :
β {π : 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] {s : Set E}
{f : E β F} {xβ : E} {m n : ββ},
ContDiffWithinAt π n f s xβ β
UniqueDiffOn π s β m + 1 β€ n β xβ β s β ContDiffWithinAt π m (fderivWithin π f s) s xβ
The theorem `ContDiffWithinAt.fderivWithin_right` states that for a nontrivially normed field `π`, a normed additive commutative group `E` that forms a normed space over `π`, another normed additive commutative group `F` that also forms a normed space over `π`, a set `s` of elements of type `E`, a function `f` from `E` to `F`, and an element `xβ` of `E`, if `f` is `n` times continuously differentiable at `xβ` within the set `s`, the set `s` has unique tangent vectors at every point, and `m + 1` is less than or equal to `n`, then `xβ` is in `s` and the derivative of `f` within `s`, `fderivWithin π f s`, is `m` times continuously differentiable at `xβ` within `s`. In simpler terms, assuming certain conditions, if a function is continuously differentiable up to a certain order, then its derivative is also continuously differentiable up to a certain order.
More concisely: If a function is `n` times continuously differentiable at a point `xβ` in a set `s` where the set has unique tangent vectors and `m + 1` is less than or equal to `n`, then the derivative of the function up to order `m` is also `m` times continuously differentiable at `xβ` within `s`.
|
ContDiffAt.fst
theorem ContDiffAt.fst :
β {π : 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] {n : ββ} {f : E β F Γ G} {x : E},
ContDiffAt π n f x β ContDiffAt π n (fun x => (f x).1) x
This theorem, `ContDiffAt.fst`, states that for any nontrivially normed field `π`, commutative additive normed groups `E`, `F`, `G` where `E`, `F`, `G` are also normed spaces over `π`, any function `f` mapping `E` to the Cartesian product of `F` and `G`, and any value `x` in `E`, if `f` is continuously differentiable of any order `n` at `x`, then the function that maps `x` to the first component `(f x).1` of `f(x)` is also continuously differentiable of the same order `n` at `x`. This means that the continuity of differentiability is preserved when post-composing `f` with the function `Prod.fst`, which extracts the first component of the pair.
More concisely: If `f: E β F Γ G` is a continuously differentiable function of order `n` on a nontrivially normed field `π` from a normed space `E` to the Cartesian product of two normed spaces `F Γ G`, then the function `x β¦ (f x).1` extracting the first component of `f(x)` is also continuously differentiable of order `n` on `E`.
|
ContDiffOn.const_smul
theorem ContDiffOn.const_smul :
β {π : 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] {n : ββ}
{R : Type u_3} [inst_5 : Semiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass π R F]
[inst_8 : ContinuousConstSMul R F] {s : Set E} {f : E β F} (c : R),
ContDiffOn π n f s β ContDiffOn π n (fun y => c β’ f y) s
The theorem states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, both of which are normed spaces over `π`, any semiring `R` that is a module over `F` and commutes with `π` under scalar multiplication, and any set `s` of elements from `E` mapping to `F` via function `f`, if the function `f` is `C^n` continuous differentiable on the set `s`, then the function that maps each element `y` in `s` to the result of scalar multiplication of a constant `c` from `R` and `f(y)` is also `C^n` continuous differentiable on `s`. Here, `C^n` denotes n-times continuously differentiable.
More concisely: For any nontrivially normed field `π`, if `f : E β Π€` is a `C^n` continuously differentiable function from a normed additive commutative group `E` to another `F`, both of which are normed spaces over `π`, and `c β R` is a constant from a semiring `R` commuting with `π` under scalar multiplication, then the function `g(y) = c * f(y)` is also `C^n` continuously differentiable on the domain of `f`.
|
ContDiffAt.continuousLinearMap_comp
theorem ContDiffAt.continuousLinearMap_comp :
β {π : 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] {f : E β F} {x : E} {n : ββ} (g : F βL[π] G),
ContDiffAt π n f x β ContDiffAt π n (βg β f) x
This theorem states that the composition of a function `f` with a continuous linear map `g` is `C^n` differentiable at a point `x` in the domain, given that the function `f` is `C^n` differentiable at that point. Here, `C^n` differentiability means the function is n times continuously differentiable, `π` is a nontrivial normed field, and `E`, `F`, and `G` are normed vector spaces over `π`. The function `f` maps `E` to `F`, while the continuous linear map `g` maps `F` to `G`.
More concisely: If `f: E β F` is `C^n` differentiable at `x β E` and `g: F β G` is a continuous linear map, then the composition `g β f: E β G` is `C^n` differentiable at `x` and `(D(g β f)(x) = Dg(f(x)) β Df(x))`, where `D` denotes the derivative.
|
ContDiffAt.neg
theorem ContDiffAt.neg :
β {π : 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] {x : E}
{n : ββ} {f : E β F}, ContDiffAt π n f x β ContDiffAt π n (fun x => -f x) x
This theorem states that if a function `f` is continuously differentiable at a point `x` to the `n`th degree over a nontrivially normed field `π`, then the negative of that function `-f` is also continuously differentiable at the same point `x` to the `n`th degree over the same field `π`. The spaces `E` and `F` are assumed to be normed additive commutative groups and normed spaces over `π`.
More concisely: If `f : E β F` is continuously differentiable to degree `n` at `x` over a nontrivially normed field `π`, then `-f` is also continuously differentiable to degree `n` at `x` over the same field `π`.
|
ContDiffOn.continuousOn_fderivWithin_apply
theorem ContDiffOn.continuousOn_fderivWithin_apply :
β {π : 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] {s : Set E}
{f : E β F} {n : ββ},
ContDiffOn π n f s β
UniqueDiffOn π s β 1 β€ n β ContinuousOn (fun p => (fderivWithin π f s p.1) p.2) (s ΓΛ’ Set.univ)
The theorem `ContDiffOn.continuousOn_fderivWithin_apply` states that if a function `f`, which maps from a normed space `E` over a non-trivially normed field `π` to another normed space `F` over the same field, is at least `C^1` continuously differentiable on a set `s` in `E`, and if `s` has unique differentials, then its bundled derivative (a function mapping a pair `(x, v)` to the derivative of `f` at `x` applied to `v`, represented as `(fderivWithin π f s p.1) p.2`) is continuous on `s` crossed with the universal set (representing all `v`). The continuity of the derivative holds for all `v` in the universal set.
More concisely: If `f` is a `C^1` continuously differentiable function from a normed space `E` to another normed space `F` over the same field, and `s` is a subset of `E` with unique differentials, then the bundled derivative `(fderivWithin π f s)` is a continuous function from `s` x `E` to `F`.
|
ContDiffWithinAt.inv
theorem ContDiffWithinAt.inv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E} {π' : Type u_4} [inst_3 : NormedField π']
[inst_4 : NormedAlgebra π π'] [inst_5 : CompleteSpace π'] {f : E β π'} {n : ββ},
ContDiffWithinAt π n f s x β f x β 0 β ContDiffWithinAt π n (fun x => (f x)β»ΒΉ) s x
This theorem, named `ContDiffWithinAt.inv`, states that for any nontrivially normed field `π`, normed additive commutative group `E`, normed space `π E`, set `s` of elements of type `E`, element `x` of type `E`, normed field `π'`, normed algebra `π π'`, and complete space `π'`, given a function `f` mapping elements of type `E` to `π'` and a natural number `n` (possibly infinity), if this function `f` is continuously differentiable within the set `s` at the point `x` to order `n`, and the value of the function `f` at the point `x` is not equal to zero, then the function which maps `x` to the reciprocal of `f(x)` will also be continuously differentiable within the set `s` at the point `x` to order `n`. In other words, the reciprocal of a function that is continuously differentiable at a point, where the function's value is non-zero, is also continuously differentiable at that point.
More concisely: If a function from a normed space to a normed field is continuously differentiable to order `n` at a point where its value is non-zero, then the reciprocal function is also continuously differentiable to order `n` at that point.
|
contDiff_prodAssoc_symm
theorem contDiff_prodAssoc_symm :
β {π : 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], ContDiff π β€ β(Equiv.prodAssoc E F G).symm
This theorem states that for any nontrivially normed field `π`, and normed add commutative groups `E`, `F`, and `G` over `π`, the natural equivalence `(E Γ F) Γ G β E Γ (F Γ G)`, represented by `Equiv.prodAssoc E F G`, is smooth when the direction of the equivalence is reversed. This means that the inverse function of the equivalence is infinitely differentiable (also referred to as `C^β` smooth or `ContDiff` in Lean) over the field `π`. Note that this theorem comes with a warning referring to remarks attached to `contDiff_prodAssoc`.
More concisely: For any nontrivially normed field `π` and normed add commutative groups `E`, `F`, and `G` over `π`, the product equivalence `Equiv.prodAssoc E F G` from `(E Γ F) Γ G` to `E Γ (F Γ G)` is infinitely differentiable when reversing the direction of the equivalence.
|
ContDiffOn.comp
theorem ContDiffOn.comp :
β {π : 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] {n : ββ} {s : Set E} {t : Set F} {g : F β G}
{f : E β F}, ContDiffOn π n g t β ContDiffOn π n f s β s β f β»ΒΉ' t β ContDiffOn π n (g β f) s
This theorem states that for differentiable functions `f` and `g` on sets `s` and `t` respectively, if `f` maps `s` into `t`, then the composition `g β f` is also differentiable on `s`. Here, differentiability is couched in terms of being continuously differentiable to any natural number or infinite order (`C^n`), denoted as `ContDiffOn π n`, where `π` is a nontrivially normed field and `n` is either a natural number or infinity. The spaces `E`, `F`, and `G` are normed additive commutative groups over `π`.
More concisely: If `f` is a differentiable function from a set `s` to a normed additive commutative group `E` over a nontrivially normed field `π`, and `g` is a differentiable function from `E` to a normed additive commutative group `G` over `π`, then the composition `g β f` is a differentiable function from `s` to `G`.
|
ContDiffWithinAt.prod_map'
theorem ContDiffWithinAt.prod_map' :
β {π : 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] {n : ββ}
{E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace π E'] {F' : Type u_4}
[inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace π F'] {s : Set E} {t : Set E'} {f : E β F} {g : E' β F'}
{p : E Γ E'},
ContDiffWithinAt π n f s p.1 β ContDiffWithinAt π n g t p.2 β ContDiffWithinAt π n (Prod.map f g) (s ΓΛ’ t) p
This theorem states that for any nontrivially normed field `π` and normed add commutative groups `E`, `F`, `E'`, `F'` with corresponding normed spaces, if we have two functions `f : E β F` and `g : E' β F'` that are `C^n` continuous within sets `s` and `t` at points `p.1` and `p.2` respectively, then the product map `(Prod.map f g)`, which applies `f` and `g` to the components of the pair, is also `C^n` continuous within the product set `(s ΓΛ’ t)` at the product point `p`. Here, `C^n` continuous refers to having continuous derivatives up to order `n`.
More concisely: Given nontrivially normed fields `π`, normed add commutative groups `E`, `F`, `E'`, `F'`, and `C^n` continuous functions `f : E β F` on `s β E` at `p.1` and `g : E' β F'` on `t β E'` at `p.2`, the product map `(Prod.map f g) : E Γ E' β F Γ F'` is `C^n` continuous on `s Γ t` at `p = (p.1, p.2)`.
|
contDiffAt_id
theorem contDiffAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ} {x : E}, ContDiffAt π n id x
This theorem states that the identity function is continuously differentiable at every point in its domain. Specifically, for any nontrivially normed field `π`, normed additive commutative group `E` (which is also a normed space over `π`), and any `x` in `E`, the identity function is `n`-times continuously differentiable at `x`. In mathematical terms, if `id` denotes the identity function, then it holds that `id β C^n(π)`, where `C^n(π)` is the class of functions that are `n`-times continuously differentiable on `π`.
More concisely: For any nontrivially normed field `π` and normed additive commutative group `E` over `π`, the identity function `id` is `n`-times continuously differentiable on `E`.
|
ContDiffAt.add
theorem ContDiffAt.add :
β {π : 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] {x : E}
{n : ββ} {f g : E β F}, ContDiffAt π n f x β ContDiffAt π n g x β ContDiffAt π n (fun x => f x + g x) x
This theorem states that if two functions `f` and `g` are `C^n` (meaning they are n-times continuously differentiable) at a particular point `x` in some normed space `E`, then their sum `f + g` is also `C^n` at the same point `x`. Here, `π` is a nontrivially normed field, `E` is a normed additively commutative group that is also a normed space over `π`, and `F` is also a normed additively commutative group that is a normed space over `π`.
More concisely: If `f` and `g` are `C^n` functions at `x` in the normed spaces `E` over the field `π`, then their sum `f + g` is also `C^n` at `x`.
|
contDiffOn_snd
theorem contDiffOn_snd :
β {π : 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] {n : ββ}
{s : Set (E Γ F)}, ContDiffOn π n Prod.snd s
This theorem states that for any non-trivially normed field `π`, normed additively commutative groups `E` and `F`, which are both normed spaces over `π`, and for any set `s` consisting of ordered pairs of elements from `E` and `F`, the second projection function `Prod.snd` is infinitely differentiable (denoted `C^β` in mathematical notation) on the set `s`. In mathematical language, this means that the function which projects an ordered pair to its second component, when applied to any point in the set `s`, has all of its derivatives exist and are continuous.
More concisely: For any non-trivially normed field `π`, and normed additively commutative groups `E` and `F` over `π`, the second projection function `Prod.snd` is infinitely differentiable on the cartesian product `E Γ F`.
|
ContDiff.neg
theorem ContDiff.neg :
β {π : 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] {n : ββ}
{f : E β F}, ContDiff π n f β ContDiff π n fun x => -f x
This theorem states that if a function `f` from `E` to `F` is `C^n` differentiable (notated as `ContDiff π n f`), where `n` is a natural number or infinity (`ββ`), `E` and `F` are normed add-commutative groups over a nontrivially normed field `π`, then the negative of this function (defined as `fun x => -f x`) is also `C^n` differentiable. Essentially, it's asserting that the property of being `C^n` differentiable is preserved under taking the negative of a function.
More concisely: If `f : E β F` is `C^n` differentiable with `E` and `F` being normed add-commutative groups over a nontrivially normed field `π`, then the negative function `-f` is also `C^n` differentiable.
|
ContDiff.continuousLinearMap_comp
theorem ContDiff.continuousLinearMap_comp :
β {π : 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] {n : ββ} {f : E β F} (g : F βL[π] G),
ContDiff π n f β ContDiff π n fun x => g (f x)
This theorem states that if we have a function `f` that is `C^n` differentiable (i.e., differentiable `n` times with a continuous `n`th derivative), and `g` is a continuous linear map, then the composition of `g` with `f` (i.e., `g(f(x))`) is also `C^n` differentiable. This composition happens on the left, meaning `g` is applied to the result of `f`. This holds for any non-trivial normed field `π`, and any normed additive commutative groups `E`, `F`, and `G`, where `f` is a function from `E` to `F` and `g` is a continuous linear map from `F` to `G`.
More concisely: If `f: E -> F` is a `C^n` differentiable function and `g: F -> G` is a continuous linear map, then the composition `g β f: E -> G` is also `C^n` differentiable.
|
ContDiff.fst
theorem ContDiff.fst :
β {π : 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] {n : ββ} {f : E β F Γ G},
ContDiff π n f β ContDiff π n fun x => (f x).1
This theorem states that for any non-trivial normed field π, normed add commutative groups E, F, G, and a function `f` that maps E to pairs (F, G), if `f` is continuously differentiable at any natural number or infinity `n`, then the function that maps an input to the first element of the pair resulting from `f` is also continuously differentiable at `n`.
More concisely: If `f:` E -> (F, G) is a continuously differentiable function at every natural number or infinity from a non-trivial normed field π into pairs of normed additive groups, then the function that maps x to the first component of f(x) is continuously differentiable at every natural number or infinity.
|
contDiffWithinAt_id
theorem contDiffWithinAt_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ} {s : Set E} {x : E}, ContDiffWithinAt π n id s x
This theorem, `contDiffWithinAt_id`, states that for any non-trivially normed field `π`, normed additive commutative group `E`, normed space over `π` and `E`, a set `s` of elements of type `E`, a point `x` in `E`, and a natural number or infinity `n`, the identity function is continuously differentiable within the set `s` at the point `x`. In other words, it expresses the fact that the identity function is as smooth as you like (up to and including infinitely differentiable) at any point in any normed vector space.
More concisely: For any non-trivially normed field `π`, normed additive commutative group `E`, and for any set `s` of elements in `E`, point `x` in `E`, and natural number or infinity `n`, the identity function on `E` is `n`-times differentiable at `x` within `s`.
|
ContDiff.sub
theorem ContDiff.sub :
β {π : 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] {n : ββ}
{f g : E β F}, ContDiff π n f β ContDiff π n g β ContDiff π n fun x => f x - g x
This theorem states that for any infinitely differentiable function (`C^n` function) `f` and `g` that map from a normed additive commutative group `E` to another normed additive commutative group `F` over a nontrivially normed field `π`, the difference function `(f - g)` is also infinitely differentiable. The theorem holds for any `n` in `ββ`, the set of natural numbers including infinity, indicating the level of differentiability.
More concisely: For any infinitely differentiable functions `f` and `g` from a normed additive commutative group `E` to another normed additive commutative group `F` over a nontrivially normed field `π`, their difference `f - g` is also infinitely differentiable.
|
ContDiff.comp_contDiffWithinAt
theorem ContDiff.comp_contDiffWithinAt :
β {π : 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] {t : Set E} {x : E} {n : ββ} {g : F β G} {f : E β F},
ContDiff π n g β ContDiffWithinAt π n f t x β ContDiffWithinAt π n (g β f) t x
The theorem `ContDiff.comp_contDiffWithinAt` states that given a set `t` of elements of type `E`, a point `x` within this set, a natural number or infinity `n`, and two functions `f` and `g` with `f` mapping from `E` to `F` and `g` mapping from `F` to `G` where `E`, `F` and `G` are normed spaces over a nontrivially normed field `π`, if `g` is continuously differentiable with respect to `π` at `n` and `f` is continuously differentiable with respect to `π` at `n` within the set `t` at the point `x`, then the composition of `g` and `f` is also continuously differentiable with respect to `π` at `n` within the set `t` at the point `x`.
More concisely: If `f` is continuously differentiable with respect to a normed field `π` at `n` within the set `t` at `x`, and `g` is continuously differentiable with respect to `π` at `n`, then the composition `g β f` is continuously differentiable with respect to `π` at `n` within the set `t` at `x`.
|
ContDiffAt.smul
theorem ContDiffAt.smul :
β {π : 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] {x : E}
{n : ββ} {f : E β π} {g : E β F},
ContDiffAt π n f x β ContDiffAt π n g x β ContDiffAt π n (fun x => f x β’ g x) x
The theorem `ContDiffAt.smul` states that for any nontrivially normed field `π`, normed additive commutative groups `E` and `F`, and normed spaces over `π` for `E` and `F`, if you have two functions `f : E β π` and `g : E β F` that are both continuously differentiable at a point `x` in `E` to the `n`th degree (where `n` can be any natural number or infinity), then the function obtained by multiplying `f(x)` and `g(x)` (scalar multiplication) is also continuously differentiable at `x` to the `n`th degree. In mathematical language, if `f` and `g` are `C^n` functions at a point, their scalar multiplication is also a `C^n` function at that point.
More concisely: If `f : E β π` and `g : E β F` are `C^n` functions at a point `x` in the nontrivially normed additive commutative groups `E` and `F` over the same field `π`, then their scalar multiplication `f(x) β g(x) : π` is also a `C^n` function at `x`.
|
ContDiffAt.mul
theorem ContDiffAt.mul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {x : E} {n : ββ} {πΈ : Type u_3} [inst_3 : NormedRing πΈ] [inst_4 : NormedAlgebra π πΈ]
{f g : E β πΈ}, ContDiffAt π n f x β ContDiffAt π n g x β ContDiffAt π n (fun x => f x * g x) x
This theorem states that if you have two functions `f` and `g` that are `C^n` at a point `x` (which means they are n-times continuously differentiable at `x`), then the product function `(fun x => f x * g x)` is also `C^n` at `x`. This is true for all nontrivially normed fields `π`, normed addition commutative groups `E`, normed spaces `π E`, normed rings `πΈ`, and normed algebras `π πΈ`.
More concisely: If `f` and `g` are `C^n` functions at a point `x` in a normed algebra `π πΈ`, then their product `f x * g x` is also `C^n` at `x`.
|
ContDiff.comp_continuousLinearMap
theorem ContDiff.comp_continuousLinearMap :
β {π : 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] {n : ββ} {f : E β F} {g : G βL[π] E},
ContDiff π n f β ContDiff π n (f β βg)
This theorem states that if you have a function `f` that is `C^n` (n-times continuously differentiable), and you compose it with a continuous linear map `g` on the right, the resulting function is still `C^n`. This holds for any non-trivially normed field `π`, normed additively commutative groups `E`, `F`, and `G`, and normed spaces over `π` constituted by `E`, `F`, and `G`. The theorem applies for any n that can be a natural number or infinity.
More concisely: If `f` is a `C^n` function and `g` is a continuous linear map, then the composition `g β f` is also a `C^n` function.
|
ContDiffOn.continuousLinearMap_comp
theorem ContDiffOn.continuousLinearMap_comp :
β {π : 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] {s : Set E} {f : E β F} {n : ββ} (g : F βL[π] G),
ContDiffOn π n f s β ContDiffOn π n (βg β f) s
This theorem states that if we have a function `f` that is `C^n` differentiable on a set `s` in a normed space, then composing `f` on the left with a continuous linear map `g` preserves this `C^n` differentiability. The `C^n` differentiability is understood in the context of a normed field `π` and normed additive commutative groups `E`, `F`, and `G` that are also normed spaces over `π`. In other words, if `f` is `C^n` differentiable on `s`, then so is `g β f` on the same set `s`, where `g β f` denotes the composition of `g` and `f`.
More concisely: If `f` is `C^n` differentiable on a set `s` in normed spaces `E`, `F`, and `G` over a normed field `π`, then the composition `g β f` is `C^n` differentiable on `s`, where `g` is a continuous linear map from `E` to `F`.
|
ContDiffWithinAt.comp_continuousLinearMap
theorem ContDiffWithinAt.comp_continuousLinearMap :
β {π : 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] {s : Set E} {f : E β F} {n : ββ} {x : G}
(g : G βL[π] E), ContDiffWithinAt π n f s (g x) β ContDiffWithinAt π n (f β βg) (βg β»ΒΉ' s) x
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` with `π` as their scalars, a set `s` of elements from `E`, a function `f` from `E` to `F`, a (possibly infinite) natural number `n`, an element `x` in `G`, and a continuous linear map `g` from `G` to `E`, if the function `f` is `n`-times continuously differentiable at the point `g(x)` within the set `s`, then the composition of `f` and `g` is `n`-times continuously differentiable at the point `x` within the preimage of the set `s` under the map `g`. In mathematical terms, $(f \circ g)$ is $C^n$ at $x$ in $g^{-1}(s)$, given that $f$ is $C^n$ at $g(x)$ in $s$.
More concisely: Given a non-trivially normed field `π`, a continuously linear map `g` from a normed additive commutative group `G` to another `E`, a continuous function `f` from `E` to a normed additive commutative group `F` that is `n`-times continuously differentiable at `g(x)` in the set `s`, then `f β g` is `n`-times continuously differentiable at `x` in `gβ»ΒΉ(s)`.
|
PartialHomeomorph.contDiffAt_symm
theorem PartialHomeomorph.contDiffAt_symm :
β {π : 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] {n : ββ}
[inst_5 : CompleteSpace E] (f : PartialHomeomorph E F) {fβ' : E βL[π] F} {a : F},
a β f.target β
HasFDerivAt (βf) (βfβ') (βf.symm a) β ContDiffAt π n (βf) (βf.symm a) β ContDiffAt π n (βf.symm) a
In simpler terms, this theorem states that if `f` is a local homeomorphism (a function from one space to another that is a homeomorphism when restricted to a small enough neighborhood of any point in its domain) and a point `a` lies in its target space, and if `f` is `n` times continuously differentiable at the point `f.symm a` (the inverse image of `a` under `f`), and if the derivative of `f` at `f.symm a` is a continuous linear equivalence (a bijective linear map between normed vector spaces that has a bounded inverse), then the inverse function `f.symm` is `n` times continuously differentiable at the point `a`.
This is a part of the inverse function theorem which assumes that we already have an inverse function. The inverse function theorem is a fundamental result in analysis which states that a smooth function that has a non-zero derivative at a point has a locally defined inverse function near that point which is also smooth.
More concisely: If a local homeomorphism `f` is `n` times continuously differentiable at the point `a` in its target space, with a continuous linear equivalence derivative at `f.symm a`, then `f.symm` is `n` times continuously differentiable at point `a` in its domain.
|
ContDiffAt.const_smul
theorem ContDiffAt.const_smul :
β {π : 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] {n : ββ}
{R : Type u_3} [inst_5 : Semiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass π R F]
[inst_8 : ContinuousConstSMul R F] {f : E β F} {x : E} (c : R),
ContDiffAt π n f x β ContDiffAt π n (fun y => c β’ f y) x
This theorem states that the scalar multiplication of a constant `c` and a differentiable function `f` of class `C^n` at a point `x` is also of class `C^n` at the same point. Here, `C^n` refers to a function that is n-times continuously differentiable. The function `f` maps from a normed additively commutative group `E` to another `F`, both of which are normed spaces over a nontrivially normed field `π`. The scalar `c` is from a semiring `R` which is a module over `F`. The multiplication between `c` and `f` is commutative and continuous. This theorem ensures that differentiable properties are maintained under scalar multiplication.
More concisely: If `f` is a differentiable function of class `C^n` from a normed additively commutative group `E` to a normed space `F` over a nontrivially normed field `π,` and `c` is a scalar from a commutative semiring `R` that is a module over `F`, then the scalar multiplication `c * f` is also a differentiable function of class `C^n` at a point `x` in `E.`
|
ContDiffOn.neg
theorem ContDiffOn.neg :
β {π : 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] {n : ββ}
{s : Set E} {f : E β F}, ContDiffOn π n f s β ContDiffOn π n (fun x => -f x) s
The theorem `ContDiffOn.neg` states that for any non-trivially normed field `π`, any normed additive commutative group `E` over `π`, any normed additive commutative group `F` over `π`, any natural number `n` or infinity, any set `s` of elements from `E`, and any function `f` from `E` to `F`, if the function `f` is continuously differentiable on the set `s` up to order `n`, then the negative of the function `f`, defined as the function that maps `x` to `-f(x)`, is also continuously differentiable on the set `s` up to order `n`. This is a fundamental fact in differential calculus.
More concisely: If a function is continuously differentiable on a set up to order n, then the negative of the function is also continuously differentiable on that set up to order n.
|
ContinuousLinearEquiv.contDiff
theorem ContinuousLinearEquiv.contDiff :
β {π : 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] {n : ββ}
(f : E βL[π] F), ContDiff π n βf
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F` (which are also normed spaces over `π`), and any natural number or infinity `n`, if `f` is a continuous linear equivalence from `E` to `F`, then the function `f` is `n`-times continuously differentiable.
More concisely: If `f` is a continuous linear equivalence between normed spaces `E` and `F` over a non-trivially normed field, then `f` is `n`-times differentiable for any natural number or infinity `n`.
|
ContDiffWithinAt.sub
theorem ContDiffWithinAt.sub :
β {π : 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] {x : E}
{n : ββ} {s : Set E} {f g : E β F},
ContDiffWithinAt π n f s x β ContDiffWithinAt π n g s x β ContDiffWithinAt π n (fun x => f x - g x) s x
The theorem `ContDiffWithinAt.sub` states that if we have two functions, `f` and `g`, that are `C^n` continuous (i.e., continuously differentiable up to the nth derivative) at a point `x` within a given set `s` in a normed space over a nontrivially normed field, then the function that is the difference of `f` and `g` is also `C^n` continuous at the same point `x` within the same set `s`. This theorem is applicable in the context of analysis in normed spaces.
More concisely: If `f` and `g` are `C^n` continuous at `x` in set `s` of a normed space over a nontrivially normed field, then `f - g` is also `C^n` continuous at `x` in `s`.
|
contDiff_snd
theorem contDiff_snd :
β {π : 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] {n : ββ},
ContDiff π n Prod.snd
The theorem `contDiff_snd` states that for any number type `π` that has a normed field structure, any types `E` and `F` that have normed additive commutative group structures and are normed spaces over `π`, and any natural number or infinity `n`, the second projection function `Prod.snd` on the product of `E` and `F` is continuously differentiable `n` times. In other words, the second component of a pair (tuple) is a function that is `C^β` or infinitely differentiable.
More concisely: For any normed field `π`, and normed additive commutative groups `E` and `F` as normed spaces over `π`, the second projection function `Prod.snd` on the product of `E` and `F` is infinitely differentiable.
|
ContDiffWithinAt.continuousLinearMap_comp
theorem ContDiffWithinAt.continuousLinearMap_comp :
β {π : 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] {s : Set E} {f : E β F} {x : E} {n : ββ}
(g : F βL[π] G), ContDiffWithinAt π n f s x β ContDiffWithinAt π n (βg β f) s x
The theorem `ContDiffWithinAt.continuousLinearMap_comp` states that for any nontrivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` with normed vector spaces over `π`, a set `s` of `E`, a function `f` from `E` to `F`, a point `x` in `E`, and a smoothness degree `n`, if a continuous linear map `g` from `F` to `G` is given, then the composition of `f` and `g` is continuously differentiable within `s` at `x` to degree `n` whenever `f` is continuously differentiable within `s` at `x` to degree `n`. This means that the continuity and smoothness of a function are preserved when it is composed with a continuous linear map.
More concisely: For any nontrivially normed fields `π` and normed vector spaces `E`, `F`, and `G` over `π`, if `g` is a continuous linear map from `F` to `G`, `f` is continuously differentiable from `E` to `F` to degree `n` at `x` in `E`, then the composition `g β f` is continuously differentiable from `E` to `G` to degree `n` at `x`.
|
ContDiffOn.comp_continuousLinearMap
theorem ContDiffOn.comp_continuousLinearMap :
β {π : 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] {s : Set E} {f : E β F} {n : ββ},
ContDiffOn π n f s β β (g : G βL[π] E), ContDiffOn π n (f β βg) (βg β»ΒΉ' s)
This theorem states that if we have a function `f` that is `C^n` differentiable on a set `s`, then the composition of `f` with a continuous linear map `g` is also `C^n` differentiable on the preimage of `s` under `g`. Here, `π`, `E`, `F`, and `G` are types equipped with additional structures such as a normed field and normed space. `n` can be a natural number or infinity, corresponding to the number of times a function can be differentiated.
More concisely: If `f: E -> F` is `C^n` differentiable on a set `s β E`, and `g: π -> G` is a continuous linear map, then `composition (g β f)` is `C^n` differentiable on `gβ»ΒΉ(s) β π`.
|
ContDiffWithinAt.neg
theorem ContDiffWithinAt.neg :
β {π : 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] {x : E}
{n : ββ} {s : Set E} {f : E β F}, ContDiffWithinAt π n f s x β ContDiffWithinAt π n (fun x => -f x) s x
The theorem `ContDiffWithinAt.neg` states that for any nontrivially normed field `π` and normed additive commutative groups `E` and `F`, both of which are normed spaces over `π`. Given a point `x` in `E`, a function `f` mapping from `E` to `F`, a subset `s` of `E`, and an order of differentiability `n`, if the function `f` is `n`-times continuously differentiable within the subset `s` at the point `x`, then the negative of the function `f` (i.e., the function `g` defined as `g(x) = -f(x)`) is also `n`-times continuously differentiable within the same subset `s` at the same point `x`. This is a generalization of the fact that the derivative of a negated function is the negation of the derivative of the original function.
More concisely: If a function is `n`-times continuously differentiable within a subset of a normed space at a point, then the negative of the function is also `n`-times continuously differentiable at that point in the same subset.
|
contDiffWithinAt_snd
theorem contDiffWithinAt_snd :
β {π : 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] {n : ββ}
{s : Set (E Γ F)} {p : E Γ F}, ContDiffWithinAt π n Prod.snd s p
This theorem states that for every non-trivially normed field `π`, normed add commutative groups `E` and `F` with `π` as their scalar field, any extended natural number `n`, a set `s` of pairs of elements from `E` and `F`, and a pair `p` of elements from `E` and `F`, the second projection function (`Prod.snd`) is `n`-times continuously differentiable within the set `s` at the point `p`. In mathematical terms, if `π` is a normed field, `E` and `F` are normed vector spaces over `π`, `n` is an extended natural number (including infinity), `s` is a subset of `E Γ F`, and `p` is a point in `E Γ F`, then the function that projects an `E Γ F` pair onto its second component is `C^n` (continuously differentiable `n` times) within `s` at `p`.
More concisely: For every non-trivially normed field `π`, normed additive groups `E` and `F` with `π` as their scalar field, extended natural number `n`, and a subset `s` of `E Γ F` and point `p` in `E Γ F`, the second projection function `Prod.snd` is `C^n` differentiable at `p` within `s` as a function from `E Γ F` to `F`.
|
ContDiffOn.sub
theorem ContDiffOn.sub :
β {π : 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] {n : ββ}
{s : Set E} {f g : E β F}, ContDiffOn π n f s β ContDiffOn π n g s β ContDiffOn π n (fun x => f x - g x) s
This theorem states that for any non-trivially normed field `π`, normed addition-commutative group `E` and `F`, a set `s` of elements from `E`, two functions `f` and `g` from `E` to `F`, and a non-negative integer or infinity `n`, if functions `f` and `g` are continuously differentiable up to order `n` on the set `s`, then the function that maps each element `x` in `E` to the difference of `f(x)` and `g(x)` is also continuously differentiable up to order `n` on `s`.
More concisely: Given a non-trivially normed field `π`, a normed additive commutative group `E`, a set `s` of elements from `E`, and functions `f` and `g` from `E` to a normed additive commutative group `F`, if `f` and `g` are continuously differentiable up to order `n` on `s`, then the function `x β¦ f(x) - g(x)` is continuously differentiable up to order `n` on `s`.
|
contDiffAt_inv
theorem contDiffAt_inv :
β (π : Type u_1) [inst : NontriviallyNormedField π] {π' : Type u_4} [inst_1 : NormedField π']
[inst_2 : NormedAlgebra π π'] [inst_3 : CompleteSpace π'] {x : π'},
x β 0 β β {n : ββ}, ContDiffAt π n Inv.inv x
The theorem `contDiffAt_inv` states that for any nontrivially normed field `π`, any normed field `π'` which is also a normed algebra over `π` and a complete space, any non-zero element `x` of `π'`, and any `n` in `ββ` (the natural numbers together with positive infinity), the function `Inv.inv` (which inverts elements of a type) is `n`-times continuously differentiable at `x`.
More concisely: For any nontrivially normed field `π`, normed field `π'` over `π` that is also a complete normed algebra, and any non-zero `x` in `π'`, the function `Inv.inv` is `n`-times continuously differentiable at `x`.
|
ContDiffAt.snd
theorem ContDiffAt.snd :
β {π : 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] {n : ββ} {f : E β F Γ G} {x : E},
ContDiffAt π n f x β ContDiffAt π n (fun x => (f x).2) x
This theorem states that given a function `f` that maps a point from a normed additive commutative group `E` over a non-trivially normed field `π` to a pair of points in normed additive commutative groups `F` and `G`, the composition of `f` with the function `Prod.snd` (which extracts the second element of the pair) is `C^n` differentiable at a point `x` in `E`, if `f` is `C^n` differentiable at `x`. In other words, if `f` is differentiable at `x`, then the function that maps `x` to the second component of `f(x)` is also differentiable at `x`.
More concisely: If `f : E β F Γ G` is `C^n` differentiable at `x β E` and `F` and `G` are normed additive commutative groups over a non-trivially normed field, then the composition `f β Prod.snd` is `C^n` differentiable at `x`.
|
ContDiffOn.smul
theorem ContDiffOn.smul :
β {π : 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] {n : ββ}
{s : Set E} {f : E β π} {g : E β F},
ContDiffOn π n f s β ContDiffOn π n g s β ContDiffOn π n (fun x => f x β’ g x) s
This theorem, named `ContDiffOn.smul`, states that if you have two functions that are continuously differentiable up to order `n` over a set `s` in the domain, then the scalar multiplication of these functions (i.e., each element of the first function multiplied by the corresponding element of the second function) is also continuously differentiable up to order `n` on that set `s`.
More formally, consider a nontrivial normed field `π`, and normed vector spaces `E` and `F` over `π`. Let `s` be a set of elements in `E`, and `f` and `g` be functions mapping from `E` to `π`. If `f` and `g` are both continuously `n` times differentiable on the set `s`, then the function obtained by multiplying `f(x)` with `g(x)` for each `x` in `E` is also continuously `n` times differentiable on `s`.
The theorem further assumes that `E` and `F` are normed additive commutative groups, and that the normed field `π` is also the scalar field for the vector spaces. This ensures that the operations of addition and scalar multiplication are well-defined and follow the necessary properties in these spaces.
More concisely: If two continuously differentiable up to order `n` functions map from a normed additive commutative group `E` to a normed field `π`, then their pointwise product is also continuously differentiable up to order `n` on `E`.
|
contDiffOn_succ_iff_deriv_of_isOpen
theorem contDiffOn_succ_iff_deriv_of_isOpen :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F} {sβ : Set π} {n : β},
IsOpen sβ β (ContDiffOn π (β(n + 1)) fβ sβ β DifferentiableOn π fβ sβ β§ ContDiffOn π (βn) (deriv fβ) sβ)
This theorem states that for any nontrivially normed field `π`, any normed additive commutative group `F` equipped with a normed space over `π`, any function `fβ` from `π` to `F`, any set `sβ` of `π`, and any natural number `n`, if `sβ` is open in the topological space of `π`, then the function `fβ` is continuously differentiable `n + 1` times on `sβ` if and only if it is differentiable on `sβ` and its derivative (formulated with `deriv`) is continuously differentiable `n` times on `sβ`. In mathematical terms, a function is $C^{(n + 1)}$ on an open domain if and only if it is differentiable there, and its derivative is $C^n$.
More concisely: For a nontrivially normed field `π`, a normed additive commutative group `F` over `π`, a function `fβ` from `π` to `F`, a set `sβ` of `π` open in its topology, the function `fβ` is `C^{(n+1)}` on `sβ` if and only if it is `C^1` on `sβ` and its derivative `deriv fβ` is `C^n` on `sβ`.
|
ContDiffWithinAt.comp_of_mem
theorem ContDiffWithinAt.comp_of_mem :
β {π : 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] {n : ββ} {s : Set E} {t : Set F} {g : F β G}
{f : E β F} (x : E),
ContDiffWithinAt π n g t (f x) β
ContDiffWithinAt π n f s x β t β nhdsWithin (f x) (f '' s) β ContDiffWithinAt π n (g β f) s x
The theorem `ContDiffWithinAt.comp_of_mem` states that for every nontrivial normed field `π`, normed additive commutative groups `E`, `F`, `G`, over the normed spaces `π`, `E`, `F` respectively, a natural number or infinity `n`, and sets `s` and `t` in `E` and `F` respectively, and functions `f` and `g` from `E` to `F` and `F` to `G` respectively. If the function `g` is continuously differentiable within the set `t` at the point `f(x)`, and the function `f` is continuously differentiable within the set `s` at the point `x`, and the set `t` is in the neighborhood of `f(x)` within `f` mapped over `s`, then the composition of `f` and `g`, denoted as `g β f`, is continuously differentiable within the set `s` at the point `x`.
In mathematical terms, this theorem comes into play when we wish to ensure that the composition of two continuously differentiable functions remains continuously differentiable under certain conditions.
More concisely: If `f` is continuously differentiable at `x` within the set `s` and `g` is continuously differentiable at `f(x)` within the set `t` with `t` in the neighborhood of `f(x)` within the image of `s`, then the composition `g β f` is continuously differentiable at `x`.
|
ContDiffOn.mul
theorem ContDiffOn.mul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {n : ββ} {πΈ : Type u_3} [inst_3 : NormedRing πΈ]
[inst_4 : NormedAlgebra π πΈ] {f g : E β πΈ},
ContDiffOn π n f s β ContDiffOn π n g s β ContDiffOn π n (fun x => f x * g x) s
This theorem states that given a nontrivially normed field `π`, a normed additively commutative group `E`, a normed space over `E` and `π`, a set `s` of elements of type `E`, a possibly infinite natural number `n`, and a normed ring `πΈ` with a normed algebra over `π`, if two functions `f` and `g` from `E` to `πΈ` are continuously differentiable `n` times on the set `s`, then their product function (where each output is the product of the outputs of `f` and `g` at the same input) is also continuously differentiable `n` times on the set `s`.
More concisely: Given a nontrivially normed field `π`, a normed additively commutative group `E`, a normed space over `π` and `E`, a set `s` of elements in `E`, a possibly infinite natural number `n`, and normed rings `πΈ` with a normed algebra over `π`, if `f` and `g` are `n`-times continuously differentiable functions from `E` to `πΈ` on `s`, then their product function is also `n`-times continuously differentiable on `s`.
|
ContDiff.fderiv_right
theorem ContDiff.fderiv_right :
β {π : 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] {f : E β F}
{m n : ββ}, ContDiff π n f β m + 1 β€ n β ContDiff π m (fderiv π f)
The theorem `ContDiff.fderiv_right` states that the Frechet derivative `fderiv π f` of a function `f` is smooth. More specifically, for any nontrivially normed field `π`, normed additive commutative groups `E` and `F` over `π`, and a function `f` from `E` to `F`, if `f` is continuously differentiable `n` times (`ContDiff π n f`), and `m + 1` is less than or equal to `n`, then the Frechet derivative of `f` is also continuously differentiable `m` times (`ContDiff π m (fderiv π f)`).
More concisely: If a function `f` is continuously differentiable of order `n` over a normed additive commutative group with values in another such group, then the Frechet derivative of `f` is also continuously differentiable of order `m` for any `m < n`.
|
ContinuousLinearMap.contDiff
theorem ContinuousLinearMap.contDiff :
β {π : 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] {n : ββ}
(f : E βL[π] F), ContDiff π n βf
This theorem states that for any continuous linear map `f` from a normed additive commutative group `E` into another normed additive commutative group `F` (both of which are also normed spaces over a nontrivially normed field `π`), the function `f` is `n`-times continuously differentiable. In other words, `f` has continuous derivatives up to order `n`, where `n` can be any natural number or infinity (`ββ`).
More concisely: For any continuous linear map between normed additive commutative groups over a nontrivially normed field, the map is infinitely differentiable.
|
LinearIsometry.norm_iteratedFDeriv_comp_left
theorem LinearIsometry.norm_iteratedFDeriv_comp_left :
β {π : 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] {n : ββ} {f : E β F} (g : F ββα΅’[π] G),
ContDiff π n f β β (x : E) {i : β}, βi β€ n β βiteratedFDeriv π i (βg β f) xβ = βiteratedFDeriv π i f xβ
This theorem states that the norm of the iterated derivative of a function composed with a linear isometry on the left is preserved. Specifically, for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G`, normed spaces over `π` for `E`, `F`, and `G`, any function `f` from `E` to `F`, a linear isometry `g` from `F` to `G`, and any natural number `n` (including infinity), if `f` is continuously differentiable up to order `n` at some point `x` in `E`, then the `i`-th derivative of the composition of `g` and `f` at `x` has the same norm as the `i`-th derivative of `f` at `x`, for any `i` less than or equal to `n`.
More concisely: For any continuously differentiable function `f: E β F` up to order `n` at `x β E`, and linear isometry `g: F β G`, the norm of the `i`-th derivative of their composition `g β f` at `x` equals the norm of the `i`-th derivative of `f` at `x`, for all `0 β€ i β€ n`.
|
ContDiffWithinAt.comp
theorem ContDiffWithinAt.comp :
β {π : 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] {n : ββ} {s : Set E} {t : Set F} {g : F β G}
{f : E β F} (x : E),
ContDiffWithinAt π n g t (f x) β ContDiffWithinAt π n f s x β s β f β»ΒΉ' t β ContDiffWithinAt π n (g β f) s x
The theorem `ContDiffWithinAt.comp` states that the composition of `C^n` functions at points within certain domains is also `C^n`, under certain conditions. More specifically, for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` with `π` as their scalar fields, any function `g` from `F` to `G`, `f` from `E` to `F`, sets `s` and `t` in `E` and `F` respectively, and a natural number `n` (or infinity), if the function `g` is `C^n` differentiable within `t` at `f(x)` and the function `f` is `C^n` differentiable within `s` at `x`, and if the set `s` is a subset of the preimage of `t` under `f`, then the composition of `g` and `f` is `C^n` differentiable within `s` at `x`.
More concisely: If functions `f : E β F` and `g : F β G` are `C^n` differentiable at `x` and `f(x)` respectively, and `s β fβ»ΒΉ(t)` where `t = f(s)`, then `g β f` is `C^n` differentiable at `x`.
|
contDiffOn_id
theorem contDiffOn_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ} {s : Set E}, ContDiffOn π n id s
This theorem, `contDiffOn_id`, states that for any non-trivially normed field `π`, any normed additive commutative group `E` that is also a normed space over `π`, any extended natural number `n`, and any set `s` of elements of type `E`, the identity function is continuously differentiable on `s` up to the `n`th derivative. In other words, the identity function maintains its smoothness up to the `n`th derivative for any elements in the given set in the given normed space.
More concisely: For any non-trivially normed field `π`, normed additive commutative group `E` over `π`, extended natural number `n`, and set `s` in `E`, the identity function is `n`-times differentiable on `s`.
|
Mathlib.Analysis.Calculus.ContDiff.Basic._auxLemma.1
theorem Mathlib.Analysis.Calculus.ContDiff.Basic._auxLemma.1 :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : β}, iteratedFDeriv π n f = iteratedFDerivWithin π n f Set.univ
This theorem states that for any nontrivially normed field `π`, any normed additive commutative group `E` and `F` which are also normed spaces over `π`, any function `f` from `E` to `F`, and any natural number `n`, the `n`-th iterated FrΓ©chet derivative of `f` over the entire domain `E` (as represented by `Set.univ`) is equal to the `n`-th iterated FrΓ©chet derivative of `f` within the universal set. In other words, taking the FrΓ©chet derivative over the whole space or within the universal set gives the same result.
More concisely: For any nontrivially normed field `π`, any normed additive commutative groups `E` and `F` over `π`, and any continuous function `f` from `E` to `F`, the `n`-th iterated Frechet derivative of `f` over the entire domain `E` equals its `n`-th iterated Frechet derivative within the universal set `Set.univ`.
|
ContDiff.fderiv_apply
theorem ContDiff.fderiv_apply :
β {π : 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] {f : E β F β G} {g k : E β F} {n m : ββ},
ContDiff π m (Function.uncurry f) β
ContDiff π n g β ContDiff π n k β n + 1 β€ m β ContDiff π n fun x => (fderiv π (f x) (g x)) (k x)
This theorem, `ContDiff.fderiv_apply`, states that for a given nontrivially normed field `π`, normed add commutative groups `E`, `F`, and `G` which are also normed spaces over `π`, functions `f : E β F β G`, `g : E β F`, `k : E β F`, and natural numbers or infinity `n` and `m`, if the uncurried version of function `f` is `m` times continuously differentiable, and both functions `g` and `k` are `n` times continuously differentiable, and `n + 1` is less than or equal to `m`, then the function `x β¦ fderiv π (f x) (g x) (k x)` is `n` times continuously differentiable over `π`. In simpler terms, it says that the derivative of a composition of smoothly varying functions is also a smoothly varying function under certain conditions.
More concisely: If the uncurried version of a composition of `m`-times continuously differentiable functions `f(x, y) : E Γ F β G` and `n`-times continuously differentiable functions `g : E β F` and `k : E β F` with `n + 1 β€ m`, then the function `x β¦ fderivβ (f x y) (g x) (k x)` is `n`-times continuously differentiable.
|
ContDiff.comp_contDiffOn
theorem ContDiff.comp_contDiffOn :
β {π : 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] {n : ββ} {s : Set E} {g : F β G} {f : E β F},
ContDiff π n g β ContDiffOn π n f s β ContDiffOn π n (g β f) s
This theorem states that if we have a continuously differentiable function `g` of any degree `n`, and another function `f` that is continuously differentiable of the same degree `n` on a set `s`, then the composition of `g` and `f` (written as `g β f`) is also continuously differentiable of degree `n` on that same set `s`. This is formalized over a nontrivially normed field `π` and normed add commutative groups `E`, `F`, `G` which are also normed spaces over `π`. The degree `n` of differentiability could be any natural number or infinity.
More concisely: If `g` is a continuously differentiable function of degree `n` and `f` is another continuously differentiable function of the same degree `n` defined on a set `s`, then the composition `g β f` is also continuously differentiable of degree `n` on `s`.
|
PartialHomeomorph.contDiffAt_symm_deriv
theorem PartialHomeomorph.contDiffAt_symm_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {n : ββ} [inst_1 : CompleteSpace π] (f : PartialHomeomorph π π)
{fβ' a : π},
fβ' β 0 β
a β f.target β HasDerivAt (βf) fβ' (βf.symm a) β ContDiffAt π n (βf) (βf.symm a) β ContDiffAt π n (βf.symm) a
The theorem `PartialHomeomorph.contDiffAt_symm_deriv` states that given a local homeomorphism `f` of a nontrivially normed field, and a point `a` in the target of `f`, if `f` is `n` times continuously differentiable at `f.symm a` (the preimage of `a` under `f`), and the derivative of `f` at `f.symm a` is not zero, then the inverse of `f` (denoted `f.symm`) is `n` times continuously differentiable at the point `a`. This theorem is part of the inverse function theorem, under the assumption that an inverse function already exists.
More concisely: If a local homeomorphism of a nontrivially normed field is `n` times continuously differentiable at the preimage of a point with non-zero derivative, then its inverse is `n` times continuously differentiable at that point.
|
ContDiffWithinAt.prod
theorem ContDiffWithinAt.prod :
β {π : 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] {x : E} {n : ββ} {s : Set E} {f : E β F} {g : E β G},
ContDiffWithinAt π n f s x β ContDiffWithinAt π n g s x β ContDiffWithinAt π n (fun x => (f x, g x)) s x
The theorem `ContDiffWithinAt.prod` states that for any normed field `π` with non-trivial norms, normed additive commutative groups `E`, `F`, and `G` with a normed vector space structure over `π`, a point `x` in `E`, a natural number `n` or infinity `ββ`, a set `s` of elements in `E`, and functions `f` and `g` mapping `E` to `F` and `G` respectively. If these functions `f` and `g` are continuously differentiable `n` times within the set `s` at the point `x`, then the function mapping `x` to the pair `(f x, g x)` is also continuously differentiable `n` times within the set `s` at the point `x`. This theorem thus asserts the compatibility of multi-variable `C^n` differentiability and the cartesian product operation on functions.
More concisely: If functions `f: E β F` and `g: E β G`, each continuously differentiable `n` times at `x` in `E`, then the function `(f, g): E β F Γ G` is also continuously differentiable `n` times at `x`.
|
ContDiffWithinAt.fderivWithin'
theorem ContDiffWithinAt.fderivWithin' :
β {π : 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] {s : Set E} {xβ : E} {m : ββ} {f : E β F β G}
{g : E β F} {t : Set F} {n : ββ},
ContDiffWithinAt π n (Function.uncurry f) (insert xβ s ΓΛ’ t) (xβ, g xβ) β
ContDiffWithinAt π m g s xβ β
(βαΆ (x : E) in nhdsWithin xβ (insert xβ s), UniqueDiffWithinAt π t (g x)) β
m + 1 β€ n β s β g β»ΒΉ' t β ContDiffWithinAt π m (fun x => fderivWithin π (f x) t (g x)) s xβ
This theorem, `ContDiffWithinAt.fderivWithin'`, is a special instance of the theorem `ContDiffWithinAt.fderivWithin''`, where it is mandated that the set `s` is a subset of the preimage of the set `t` under the function `g`. Given a non-trivially normed field `π`, normed additive commutative groups `E`, `F`, `G` equipped with a normed space structure over `π`, a set `s` of elements of type `E`, an element `xβ` of type `E`, extended natural numbers `m` and `n`, and functions `f` from `E` to `F β G` and `g` from `E` to `F`, the theorem states that if the function `f`, when uncurried, is `n` times continuously differentiable at the point `(xβ, g xβ)` within the set `insert xβ s ΓΛ’ t`, and the function `g` is `m` times continuously differentiable at the point `xβ` within the set `s`, and if for all `x` in a neighborhood of `xβ` within `insert xβ s`, the set `t` has unique tangent spaces at `g x`, and if `m + 1` is less than or equal to `n`, and if `s` is a subset of the preimage of `t` under `g`, then the function that maps `x` to the derivative of `f x` at `g x` within `t` is `m` times continuously differentiable at `xβ` within `s`.
More concisely: If `f` is an `n`-times continuously differentiable function from `E Γ F` to `G` with `f(x, y) = g(x) f'(x, y)` for some `g: E β F` and `n-times` continuously differentiable `g` on a neighborhood of `xβ` in `E`, `s β E` a subset of the preimage of `t β F` under `g`, and `m < n` with `m` times continuously differentiable `g` at `xβ`, then the derivative function of `f` at `g(xβ)` within `t` is `m`-times continuously differentiable at `xβ` on `s`.
|
contDiffOn_succ_iff_derivWithin
theorem contDiffOn_succ_iff_derivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F} {sβ : Set π} {n : β},
UniqueDiffOn π sβ β
(ContDiffOn π (β(n + 1)) fβ sβ β DifferentiableOn π fβ sβ β§ ContDiffOn π (βn) (derivWithin fβ sβ) sβ)
The theorem `contDiffOn_succ_iff_derivWithin` asserts that for any normed field `π`, normed add commutative group `F`, function `fβ` from `π` to `F`, set `sβ` of `π`, and natural number `n`, if the set `sβ` has unique differentials, then the function `fβ` is continuously differentiable `n + 1` times on `sβ` if and only if it is differentiable on `sβ` and its derivative (expressed with `derivWithin`) is continuously differentiable `n` times on `sβ`. In other words, a function has `n + 1` continuous derivatives in a domain with unique derivatives precisely when it is differentiable in that domain, and its derivative is continuously differentiable `n` times.
More concisely: A function from a normed field to a normed add commutative group is `(n+1)` times continuously differentiable on a set with unique differentials if and only if it is differentiable on that set and its derivative, expressed with `derivWithin`, is `n` times continuously differentiable on that set.
|
ContDiffWithinAt.div
theorem ContDiffWithinAt.div :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E} [inst_3 : CompleteSpace π] {f g : E β π} {n : ββ},
ContDiffWithinAt π n f s x β
ContDiffWithinAt π n g s x β g x β 0 β ContDiffWithinAt π n (fun x => f x / g x) s x
The theorem `ContDiffWithinAt.div` states that for any non-trivially normed field π, normed add commutative group E, normed space over π, set of elements from E, point in E, complete space π, two functions from E to π, and natural number or infinity, given the conditions that the functions are continuously differentiable within the set at the point and the second function at the point is not zero, then the function which is the ratio of first function to the second is also continuously differentiable within the set at the point.
More concisely: If two continuously differentiable functions from a normed space into a non-trivially normed field, with the second function not being the zero function at a point in a complete normed space, then their quotient is also continuously differentiable at that point.
|
contDiffWithinAt_fst
theorem contDiffWithinAt_fst :
β {π : 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] {n : ββ}
{s : Set (E Γ F)} {p : E Γ F}, ContDiffWithinAt π n Prod.fst s p
The theorem `contDiffWithinAt_fst` asserts that for any non-trivially normed field `π`, normed add commutative group `E` and `F` with a normed space over `π`, and for any set `s` of ordered pairs from `E` and `F` along with a point `p` in `E Γ F`, the first projection function (`Prod.fst`) is continuously differentiable of any order within the domain `s` at the point `p`. Here, `n : ββ` denotes the order of differentiability and `ContDiffWithinAt π n Prod.fst s p` denotes that the function `Prod.fst` is `n`-times continuously differentiable at the point `p` within the set `s`.
More concisely: For any non-trivially normed field `π`, normed add commutative groups `E` and `F`, and a set `s` of ordered pairs from `E Γ F` with a point `p` in `E Γ F`, the first projection function `Prod.fst` is `n`-times continuously differentiable at `p` within `s` for any `n : ββ`.
|
LinearIsometryEquiv.norm_iteratedFDeriv_comp_left
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left :
β {π : 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) (x : E) (i : β),
βiteratedFDeriv π i (βg β f) xβ = βiteratedFDeriv π i f xβ
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` over `π`, a linear isometry equivalence `g` between `F` and `G`, a function `f` from `E` to `F`, an element `x` of `E`, and a natural number `i`, the norm of the `i`-th derivative of the function `f` composed with `g` at the point `x` is equal to the norm of the `i`-th derivative of the function `f` at the point `x`. In other words, composition with a linear isometry equivalence on the left side doesn't change the norm of the iterated derivative.
More concisely: For any non-trivially normed field `π`, and linear isometry equivalences `g` between normed additive commutative groups `F` and `G` over `π`, the norm of the `i`-th derivative of the composite function `f β g` equals the norm of the `i`-th derivative of `f` at every point `x` in the domain of `f`.
|
ContDiffOn.prod
theorem ContDiffOn.prod :
β {π : 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] {n : ββ} {s : Set E} {f : E β F} {g : E β G},
ContDiffOn π n f s β ContDiffOn π n g s β ContDiffOn π n (fun x => (f x, g x)) s
The theorem `ContDiffOn.prod` states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, `G` with `E` being a normed space over `π`, `F` and `G` being normed spaces over `π`, and for any set `s` of elements of type `E`, functions `f` and `g` from `E` to `F` and `G` respectively, if both `f` and `g` are `C^n` differentiable on `s`, then the function mapping `x` to the pair `(f(x), g(x))` is also `C^n` differentiable on `s`. In other words, the cartesian product of `C^n` differentiable functions is also `C^n` differentiable. The `C^n` notation is used to denote n-times continuously differentiable functions.
More concisely: If `f` and `g` are `C^n` differentiable functions from a non-trivially normed vector space to their respective normed spaces, then the function mapping `x` to the pair `(f(x), g(x))` is also `C^n` differentiable.
|
ContinuousLinearMap.iteratedFDeriv_comp_left
theorem ContinuousLinearMap.iteratedFDeriv_comp_left :
β {π : 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] {n : ββ} {f : E β F} (g : F βL[π] G),
ContDiff π n f β
β (x : E) {i : β},
βi β€ n β iteratedFDeriv π i (βg β f) x = g.compContinuousMultilinearMap (iteratedFDeriv π i f x)
This theorem states that for any non-trivially normed field π, if you have a continuous differentiable function `f` mapping from a normed add commutative group `E` to another `F`, and a continuous linear map `g` from `F` to another normed add commutative group `G`, then the iterated derivative of the composition of `g` with `f` is equivalent to applying the linear map `g` to the iterated derivative of `f`. This holds for any point `x` in `E` and any natural number `i` less than or equal to `n`, where `n` is the order of differentiation.
More concisely: For any continuous differentiable function `f` from a normed add commutative group `E` to another `F`, and a continuous linear map `g` from `F` to a normed add commutative group `G`, the `i`-th derivative of `g β f` at a point `x` in `E` is equal to `g` applied to the `i`-th derivative of `f` at `x`.
|
ContDiffAt.fst''
theorem ContDiffAt.fst'' :
β {π : 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] {n : ββ} {f : E β G} {x : E Γ F},
ContDiffAt π n f x.1 β ContDiffAt π n (fun x => f x.1) x
This theorem states that for any non-trivially normed field `π`, normed add commutative groups `E`, `F`, and `G` that are also normed vector spaces over `π`, any function `f` from `E` to `G`, and any point `x` in the Cartesian product of `E` and `F`, if the function `f` is continuously differentiable of any order `n` at the first component of `x`, then the function obtained by precomposing `f` with the function that projects to the first component (`Prod.fst`) is also continuously differentiable of the same order `n` at `x`.
More concisely: If `f` is continuously differentiable of order `n` at the first component of `x` in the function space `π^E β π^G`, then the composition `f β Proj.fst` is also continuously differentiable of order `n` at `x` in the Cartesian product `E Γ F`, where `Proj.fst` is the projection function onto the first component.
|
contDiffAt_map_inverse
theorem contDiffAt_map_inverse :
β {π : 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] {n : ββ}
[inst_5 : CompleteSpace E] (e : E βL[π] F), ContDiffAt π n ContinuousLinearMap.inverse βe
The theorem states that for any continuous linear equivalence `e` between two Banach spaces `E` and `F` over a non-trivially normed field `π`, the operation of inversion is `C^n`-differentiable at every point for all `n`. In other words, the inverse of the continuous linear map is continuously differentiable of any order.
More concisely: For any continuous linear equivalence between Banach spaces over a non-trivially normed field, the inverse map is continuously differentiable of any order.
|
contDiffAt_fst
theorem contDiffAt_fst :
β {π : 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] {n : ββ}
{p : E Γ F}, ContDiffAt π n Prod.fst p
This theorem states that for any point `p` in the product of two normed spaces `E` and `F` over a nontrivially normed field `π`, the first projection function `Prod.fst` is continuously differentiable at `p` to any order `n`. This means that all derivatives of the projection function up to order `n` exist and are continuous at point `p`. In mathematical terms, if `p : E Γ F`, then `Prod.fst : E Γ F β E` is a `C^β` function at `p`.
More concisely: The first projection function of a product of two normed spaces is continuously differentiable to any order at any point in the product space.
|
ContDiffAt.fderiv_right
theorem ContDiffAt.fderiv_right :
β {π : 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] {f : E β F}
{xβ : E} {m n : ββ}, ContDiffAt π n f xβ β m + 1 β€ n β ContDiffAt π m (fderiv π f) xβ
The theorem `ContDiffAt.fderiv_right` states that if a function `f` is `n` times continuously differentiable at a point `xβ` in a normed space over a nontrivially normed field `π`, and `m + 1` is less than or equal to `n`, then the derivative of `f` (as defined by `fderiv π f`) is `m` times continuously differentiable at `xβ`. This means that the derivative of a smoothly varying function is itself smooth.
More concisely: If a function `f` is `n` times continuously differentiable at a point `xβ` in a normed space over a nontrivially normed field `π`, then its derivative is `(n-m)` times continuously differentiable at `xβ`, where `m` is a non-negative integer less than `n`.
|
contDiffOn_top_iff_deriv_of_isOpen
theorem contDiffOn_top_iff_deriv_of_isOpen :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F} {sβ : Set π},
IsOpen sβ β (ContDiffOn π β€ fβ sβ β DifferentiableOn π fβ sβ β§ ContDiffOn π β€ (deriv fβ) sβ)
This theorem states that for any type `π`, which is a field with a nontrivial norm, and any type `F`, which is a normed additive commutative group over the field `π`, a function `fβ` from `π` to `F` is infinitely continuously differentiable (`C^β`) on an open set `sβ` if and only if it is differentiable on `sβ` and its derivative, formulated with `deriv`, is also infinitely continuously differentiable on `sβ`. This essentially links the concepts of differentiability and continuous differentiability for functions on open sets in the context of normed fields.
More concisely: A function `fβ` from a field `π` to a normed additive commutative group `F` over `π` is infinitely continuously differentiable on an open set `sβ` if and only if it is differentiable on `sβ` and its derivative is also infinitely continuously differentiable on `sβ`.
|
contDiff_fst
theorem contDiff_fst :
β {π : 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] {n : ββ},
ContDiff π n Prod.fst
The theorem `contDiff_fst` states that for any non-trivial normed field `π`, and any normed additive commutative groups `E` and `F` that are also normed spaces over `π`, the first projection function, `Prod.fst`, is infinitely differentiable (`C^β`). This applies for every smoothness class `n`, represented as a natural number or infinity (`ββ`).
More concisely: For any non-trivial normed field `π` and normed additive commutative groups `E` and `F` over `π` that are normed spaces, the first projection function `Prod.fst` from `E Γ F` to `E` is infinitely differentiable.
|
contDiff_const
theorem contDiff_const :
β {π : 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] {n : ββ}
{c : F}, ContDiff π n fun x => c
This theorem states that for any nontrivially normed field `π`, normed addative commutative group `E` and `F`, and any constant `c` of type `F`, the function that maps any element of `E` to `c` is continuously differentiable of any order `n`, denoted as `ContDiff π n`. In other words, constants are infinitely differentiable (`C^β`).
More concisely: For any nontrivially normed field `π`, any normed additive commutative group `E`, and any constant `c` in `π`, the constant function mapping `E` to `c` is infinitely differentiable.
|
contDiff_id
theorem contDiff_id :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ}, ContDiff π n id
This theorem states that the identity function is continuously differentiable an infinite number of times. More formally, for any non-trivial normed field π and any normed additive commutative group E that is also a normed space over π, the identity function is continuously differentiable at every point, to any order n in ββ (the extended natural numbers, including positive infinity).
More concisely: For any non-trivial normed field π and normed additive commutative group E that is also a normed space over π, the identity function on E is continuously differentiable to any order in the extended natural numbers.
|
contDiff_mul
theorem contDiff_mul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {n : ββ} {πΈ : Type u_3} [inst_1 : NormedRing πΈ]
[inst_2 : NormedAlgebra π πΈ], ContDiff π n fun p => p.1 * p.2
This theorem states that for any nontrivially normed field `π`, natural number `n`, and normed ring `πΈ` that is also a normed algebra over `π`, the function that multiplies a pair of elements from `πΈ` is `n`-times continuously differentiable. In mathematical terms, given any pair of elements in `πΈ`, the function which multiplies these elements is subject to `n` rounds of continuous differentiation.
More concisely: For any nontrivially normed field `π`, natural number `n`, and normed ring `πΈ` that is also a normed algebra over `π`, the multiplication function on `πΈ` is `n`-times continuously differentiable.
|
contDiffOn_fderivWithin_apply
theorem contDiffOn_fderivWithin_apply :
β {π : 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] {m n : ββ}
{s : Set E} {f : E β F},
ContDiffOn π n f s β
UniqueDiffOn π s β m + 1 β€ n β ContDiffOn π m (fun p => (fderivWithin π f s p.1) p.2) (s ΓΛ’ Set.univ)
This theorem states that given a function `f` from `E` to `F` which is continuously differentiable `n` times (`ContDiffOn π n f s`) on a set `s` of `E` where `s` has unique differential properties (`UniqueDiffOn π s`), if `m + 1` is less than or equal to `n`, then the derivative function (given by `(fderivWithin π f s p.1) p.2`) is continuously differentiable `m` times. Here, the derivative function is applied on the Cartesian product of `s` and the universal set. So essentially, the theorem is describing a rule about how often a derivative of a continuously differentiable function can be found to be continuously differentiable itself.
More concisely: Given a continuously differentiable function `f` from `E` to `F` on a set `s` with unique differential properties, if `f` is `n` times differentiable on `s`, then its derivative function is `m` times differentiable for any `m` with `m < n`.
|
Continuous.fderiv
theorem Continuous.fderiv :
β {π : 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] {f : E β F β G} {g : E β F} {n : ββ},
ContDiff π n (Function.uncurry f) β Continuous g β 1 β€ n β Continuous fun x => fderiv π (f x) (g x)
The theorem `Continuous.fderiv` states that for any nontrivially normed field `π`, normed add commutative groups `E`, `F`, and `G`, and functions `f : E β F β G` and `g : E β F`, if the uncurried function `f` is continuously differentiable `n` times, `g` is continuous, and `n` is greater or equal to one, then the function `x β¦ fderiv π (f x) (g x)` is continuous. Here `fderiv π (f x) (g x)` represents the derivative of the function `f` at the point `g(x)` in the field `π`, and `Continuous` denotes the property of a function where small changes in the input lead to small changes in the output. This theorem ties together the concepts of continuity, differentiation, and function composition in the context of normed vector spaces.
More concisely: If `f : E β F β G` is a continuously differentiable n-times function between two normed add commutative groups with `g : E β F` being continuous, then the function `x mapsto fderiv (π) (fx) (gx)` is continuous, where `π` is a nontrivially normed field.
|
contDiff_succ_iff_deriv
theorem contDiff_succ_iff_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F} {n : β},
ContDiff π (β(n + 1)) fβ β Differentiable π fβ β§ ContDiff π (βn) (deriv fβ)
The theorem `contDiff_succ_iff_deriv` states that for any nontrivially normed field `π`, any normed add commutative group `F` that is also a normed space over `π`, any function `fβ` from `π` to `F`, and any natural number `n`, the function `fβ` is continuously differentiable up to level `n + 1` if and only if the function `fβ` is differentiable and its derivative (expressed using the `deriv` function) is continuously differentiable up to level `n`. Essentially, this theorem connects the concept of a function being continuously differentiable at a certain level with the differentiability of the function and its derivatives.
More concisely: A function from a nontrivially normed field to a normed add commutative group, which is both differentiable and has a continuously differentiable derivative up to level `n`, is continuously differentiable up to level `n+1`.
|
ContDiffAt.fst'
theorem ContDiffAt.fst' :
β {π : 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] {n : ββ} {f : E β G} {x : E} {y : F},
ContDiffAt π n f x β ContDiffAt π n (fun x => f x.1) (x, y)
This theorem states that if a function `f` from a normed additive commutative group `E` to another normed additive commutative group `G` over a non-trivially normed field `π` is differentiable to any degree `n` at a point `x` in `E`, then the new function that applies `f` to the first component of a pair `(x,y)` is also differentiable to the same degree `n` at the point `(x,y)`. This implies that the differentiability of `f` is preserved when it is precomposed with the function `Prod.fst` that extracts the first component of a pair.
More concisely: If `f: E β G` is differentiable to degree `n` at `x β E` in the normed additive commutative groups `E` and `G` over a non-trivially normed field `π`, then the function `g(x, y) = f(x)` is differentiable to degree `n` at `(x, y) β E Γ E`.
|
ContDiff.compβ
theorem ContDiff.compβ :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {G : Type uG} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace π G] {n : ββ}
{Eβ : Type u_3} {Eβ : Type u_4} [inst_5 : NormedAddCommGroup Eβ] [inst_6 : NormedAddCommGroup Eβ]
[inst_7 : NormedSpace π Eβ] [inst_8 : NormedSpace π Eβ] {g : Eβ Γ Eβ β G} {fβ : F β Eβ} {fβ : F β Eβ},
ContDiff π n g β ContDiff π n fβ β ContDiff π n fβ β ContDiff π n fun x => g (fβ x, fβ x)
The theorem `ContDiff.compβ` states that for any non-trivially normed field π, two functions `fβ` and `fβ` from a normed add commutative group F to normed add commutative groups Eβ and Eβ respectively, and a function `g` from the Cartesian product of Eβ and Eβ to a normed add commutative group G, if `g`, `fβ`, and `fβ` are continuously differentiable up to order `n`, then the composition function `x => g (fβ x, fβ x)` is also continuously differentiable up to order `n`.
More concisely: If two continuously differentiable up to order `n` functions from a normed add commutative group to other normed add commutative groups have values in the domain of a third continuously differentiable up to order `n` function, then their composition is also continuously differentiable up to order `n`.
|
iteratedFDerivWithin_add_apply'
theorem iteratedFDerivWithin_add_apply' :
β {π : 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] {s : Set E}
{x : E} {i : β} {f g : E β F},
ContDiffOn π (βi) f s β
ContDiffOn π (βi) g s β
UniqueDiffOn π s β
x β s β
iteratedFDerivWithin π i (fun x => f x + g x) s x =
iteratedFDerivWithin π i f s x + iteratedFDerivWithin π i g s x
The theorem `iteratedFDerivWithin_add_apply'` states that for any two functions `f` and `g`, defined in a normed space over a non-trivially normed field, and for any integer `i`, if both `f` and `g` are `i` times continuously differentiable on a set `s` in the normed space, and `s` is a unique differentiable set, then the `i`-th iterated derivative of the sum of `f` and `g` at a point `x` in `s` is equal to the sum of the `i`-th iterated derivatives of `f` and `g` at `x`. This theorem is a formalization of the rule of differentiation for the sum of two functions.
More concisely: If two functions `f` and `g` are `i`-times differentiable on a unique differentiable set `s` in a normed space over a non-trivially normed field, then the `i`-th iterated derivative of their sum equals the sum of their `i`-th iterated derivatives at any point `x` in `s`.
|
ContDiffWithinAt.fderivWithin
theorem ContDiffWithinAt.fderivWithin :
β {π : 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] {s : Set E} {xβ : E} {m : ββ} {f : E β F β G}
{g : E β F} {t : Set F} {n : ββ},
ContDiffWithinAt π n (Function.uncurry f) (s ΓΛ’ t) (xβ, g xβ) β
ContDiffWithinAt π m g s xβ β
UniqueDiffOn π t β
m + 1 β€ n β xβ β s β s β g β»ΒΉ' t β ContDiffWithinAt π m (fun x => fderivWithin π (f x) t (g x)) s xβ
This theorem, a special case of `ContDiffWithinAt.fderivWithin`, states that for a non-trivially normed field `π`, normed additively commutative groups `E`, `F`, and `G` that are normed spaces over `π`, a set `s` in `E`, an element `xβ` in `E`, a function `f` from `E` to `F` to `G`, a function `g` from `E` to `F`, a set `t` in `F`, and elements `m` and `n` in `ββ` (either a natural number or infinity), if the uncurried version of `f` is continuously differentiable within the cartesian product of `s` and `t` at the pair `(xβ, g xβ)` of order `n`, `g` is continuously differentiable within `s` at `xβ` of order `m`, `t` is a set where all elements have unique derivatives, `m` plus one is less than or equal to `n`, `xβ` is an element of `s`, and `s` is a subset of the preimage of `t` under `g`, then the function that maps `x` to the derivative of `(f x)` within `t` at `(g x)` is continuously differentiable within `s` at `xβ` of order `m`.
More concisely: If `f: E -> F -> G` is a continuously differentiable function, `g: E -> F` is a function with unique derivatives, `xβ β s β E`, `s β gβ»ΒΉ(t)`, `g` is continuously differentiable at `xβ`, and `m < n`, then the derivative of `f` at `(xβ, g xβ)` is a continuously differentiable function from `s` to `G` of order `m`.
|
contDiff_prodAssoc
theorem contDiff_prodAssoc :
β {π : 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], ContDiff π β€ β(Equiv.prodAssoc E F G)
This theorem states that for any nontrivially normed field (`π`), and normed additive commutative groups `E`, `F`, and `G` that are also normed spaces over `π`, the natural equivalence that reassociates the product of types, `(E Γ F) Γ G` to `E Γ (F Γ G)`, is smoothly differentiable with respect to `π`. In other words, the transformation that rearranges the product of these three types is infinitely continuously differentiable.
However, the warning suggests that if you think you need this theorem, you might be able to simplify your proof by reformulating the lemma that you're about to apply, as suggested in the note titled "continuity lemma statement".
More concisely: The natural equivalence between the product types `(E Γ F) Γ G` and `E Γ (F Γ G)` of two normed additive commutative groups `E`, `F`, and `G` over a nontrivially normed field `π` is smoothly differentiable.
|
HasFTaylorSeriesUpToOn.prod
theorem HasFTaylorSeriesUpToOn.prod :
β {π : 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] {s : Set E} {f : E β F} {n : ββ}
{p : E β FormalMultilinearSeries π E F},
HasFTaylorSeriesUpToOn n f p s β
β {g : E β G} {q : E β FormalMultilinearSeries π E G},
HasFTaylorSeriesUpToOn n g q s β
HasFTaylorSeriesUpToOn n (fun y => (f y, g y)) (fun y k => (p y k).prod (q y k)) s
This theorem states that given two functions `f` and `g`, if they both have a Taylor series representation `p` and `q` respectively within a set `s`, then the Cartesian product of `f` and `g` also has a Taylor series representation within the same set `s`. This new Taylor series is the Cartesian product of the Taylor series `p` and `q`. This is true for any set `s` and for any functions `f` and `g` with outputs in normed additive commutative group over a nontrivially normed field `π`, and inputs in a normed vector space over `π`.
More concisely: Given functions `f : βββ` and `g : βββ` with Taylor series `p` and `q` respectively within a normed vector space `s` over a nontrivially normed field `π`, their pointwise product `f Γ g` also has a Taylor series `p Γ q` within `s`.
|
ContDiffAt.div
theorem ContDiffAt.div :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {x : E} [inst_3 : CompleteSpace π] {f g : E β π} {n : ββ},
ContDiffAt π n f x β ContDiffAt π n g x β g x β 0 β ContDiffAt π n (fun x => f x / g x) x
This theorem states that for any nontrivially normed field `π` and normed add commutative group `E` that is a normed space over `π`, and for any point `x` in `E` and two functions `f` and `g` from `E` to `π`, if `f` and `g` are continuously differentiable at `x` of any order `n` (can be a natural number or infinity), and if `g(x)` is not zero, then the function defined by the quotient of `f(x)` by `g(x)` is also continuously differentiable at `x` of the same order `n`.
More concisely: If `f` and `g` are continuously differentiable functions of order `n` from a normed space `E` over a nontrivially normed field `π` to `π`, with `g(x) β 0`, then the quotient function `f / g` is also continuously differentiable of order `n` at `x`.
|
ContDiffAt.prod
theorem ContDiffAt.prod :
β {π : 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] {x : E} {n : ββ} {f : E β F} {g : E β G},
ContDiffAt π n f x β ContDiffAt π n g x β ContDiffAt π n (fun x => (f x, g x)) x
The theorem `ContDiffAt.prod` states that if two functions `f` and `g` are continuously differentiable up to order `n` at a point `x` in some normed space `E`, then the cartesian product of these functions, represented as a function mapping `x` to `(f x, g x)`, is also continuously differentiable up to the same order `n` at `x`. These functions and spaces are all over some field `π` that is nontrivially normed.
More concisely: If functions `f` and `g` are continuously differentiable up to order `n` at a point `x` in a normed space `E` over a nontrivially normed field `π`, then their cartesian product `(x β¦ (f x, g x))` is also continuously differentiable up to order `n` at `x`.
|
ContDiffAt.snd''
theorem ContDiffAt.snd'' :
β {π : 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] {n : ββ} {f : F β G} {x : E Γ F},
ContDiffAt π n f x.2 β ContDiffAt π n (fun x => f x.2) x
The theorem `ContDiffAt.snd''` states that for any nontrivially normed field `π`, normed add commutative groups `E`, `F`, and `G` which are also normed spaces over `π`, an extended natural number `n`, a function `f` from `F` to `G`, and a point `x` in the Cartesian product of `E` and `F`, if the function `f` is continuously differentiable of order `n` at the second component of `x`, then the function obtained by precomposing `f` with the projection on the second component (`Prod.snd`) is also continuously differentiable of order `n` at `x`. In other words, the differentiability of `f` at a point in `F` implies the differentiability of `f β Prod.snd` at a corresponding point in `E Γ F`.
More concisely: If `f` is a function continuously differentiable of order `n` at a point `x` in the product of two normed spaces `E` and `F` over a nontrivially normed field `π`, then the composition `f β Proj.snd` is also continuously differentiable of order `n` at `x`, where `Proj.snd` is the projection on the second component.
|
contDiffAt_const
theorem contDiffAt_const :
β {π : 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] {x : E}
{n : ββ} {c : F}, ContDiffAt π n (fun x => c) x
This theorem, `contDiffAt_const`, states that for any nontrivially normed field `π`, normed additive commutative group `E` that forms a normed space over `π`, another normed additive commutative group `F` that also forms a normed space over `π`, any element `x` of `E`, any natural number or infinity `n`, and any element `c` of `F`, the function that maps every element to `c` (i.e., a constant function) is continuously differentiable at the point `x` at the level `n`.
More concisely: For any normed fields `π`, normed additive commutative groups `E` and `F`, and a constant function `f : E β F` with `f(x) = c` for all `x β E`, the function `f` is continuously differentiable at `x β E` for any `x β E` and any natural number or infinity `n` in the sense of `π`-normed spaces.
|
ContDiffWithinAt.smul
theorem ContDiffWithinAt.smul :
β {π : 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] {x : E}
{n : ββ} {s : Set E} {f : E β π} {g : E β F},
ContDiffWithinAt π n f s x β ContDiffWithinAt π n g s x β ContDiffWithinAt π n (fun x => f x β’ g x) s x
This theorem states that if we have two functions `f` and `g` that map from a normed vector space `E` to a non-trivially normed field `π` and a normed vector space `F` respectively, and both `f` and `g` are continuously differentiable up to a certain degree `n` within a set `s` at a point `x`, then the scalar multiplication of `f` and `g` (defined as `f x β’ g x`) is also continuously differentiable to the same degree `n` within the same set `s` at the same point `x`. Here, continuous differentiability is defined in the sense of the mathematical field of analysis, specifically, in the context of normed vector spaces.
More concisely: If `f : E β β` and `g : E β F` are continuously differentiable up to degree `n` at `x β s` in the normed vector spaces `E` and `F` respectively, then the composition `f β’ g : E β β` is also continuously differentiable up to degree `n` at `x`.
|
ContDiffWithinAt.mul
theorem ContDiffWithinAt.mul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {x : E} {n : ββ} {πΈ : Type u_3} [inst_3 : NormedRing πΈ] [inst_4 : NormedAlgebra π πΈ]
{s : Set E} {f g : E β πΈ},
ContDiffWithinAt π n f s x β ContDiffWithinAt π n g s x β ContDiffWithinAt π n (fun x => f x * g x) s x
This theorem states that the product of two continuously differentiable (`C^n`) functions within a set at a certain point, is also continuously differentiable at this point within this set. In more detail, given a nontrivially normed field `π`, a normed additive commutative group `E` which is a normed space over `π`, a point `x` in `E`, `n` which can be any natural number or infinity, a normed ring `πΈ` that is a normed algebra over `π`, a set `s` of elements of type `E`, and two functions `f` and `g` mapping from `E` to `πΈ`, if both `f` and `g` are continuously differentiable within `s` at `x`, then the function defined by the product of `f` and `g` is also continuously differentiable within `s` at `x`.
More concisely: If two continuously differentiable functions map a normed vector space to its associated algebra, then their product is also continuously differentiable at a given point in the domain.
|
Homeomorph.contDiff_symm
theorem Homeomorph.contDiff_symm :
β {π : 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] {n : ββ}
[inst_5 : CompleteSpace E] (f : E ββ F) {fβ' : E β E βL[π] F},
(β (a : E), HasFDerivAt (βf) (β(fβ' a)) a) β ContDiff π n βf β ContDiff π n βf.symm
The theorem `Homeomorph.contDiff_symm` states that if `f` is a homeomorphism that is `n` times continuously differentiable, and the derivative of `f` at each point is a continuous linear equivalence, then the inverse function of `f` is also `n` times continuously differentiable. This theorem is a part of the inverse function theorem, and it operates under the assumption that an inverse function already exists. The mentioned homeomorphism `f` is a mapping between two normed vector spaces `E` and `F` over a nontrivially normed field `π`, and `n` is a natural number or infinity denoting the number of times the function is differentiable.
More concisely: If `fοΌE β F` is a homeomorphism that is `n` times continuously differentiable with continuous linear derivatives, then its inverse is also `n` times continuously differentiable.
|
ContDiff.const_smul
theorem ContDiff.const_smul :
β {π : 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] {n : ββ}
{R : Type u_3} [inst_5 : Semiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass π R F]
[inst_8 : ContinuousConstSMul R F] {f : E β F} (c : R), ContDiff π n f β ContDiff π n fun y => c β’ f y
The theorem `ContDiff.const_smul` states that given a non-trivially normed field π, normed add commutative groups E and F, a normed space π E, a normed space π F, a semiring R, a module R F, a `C^n` function `f` from E to F, and a constant scalar `c` from semiring `R`, if the function `f` is continuously differentiable up to order `n`, then the function resulting from scalar multiplication of `f` by `c` is also continuously differentiable up to the same order `n`. In other words, multiplying a `C^n` function by a constant does not change its differentiability order.
More concisely: If `f` is a `C^n` function from a normed add commutative group `E` to another normed add commutative group `F` over a non-trivially normed field `π`, then the scalar multiplication of `f` by a constant `c` from a semiring `R` preserves its differentiability order `n`.
|
contDiffOn_fst
theorem contDiffOn_fst :
β {π : 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] {n : ββ}
{s : Set (E Γ F)}, ContDiffOn π n Prod.fst s
The theorem `contDiffOn_fst` states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, and a set `s` of pairs of elements from `E` and `F`, the first projection function `Prod.fst`, which extracts the first element of each pair in the set, is continuously differentiable of order `n` on `s`. Here, `n` can be any natural number or β, meaning the function is infinitely differentiable. In mathematical terms, if we denote the first projection function as Οβ: E Γ F β E, the theorem states that Οβ β CβΏ(E Γ F, E), for all n in β βͺ {β}.
More concisely: For any non-trivially normed field π, normed additive commutative groups E and F, and set s of pairs from E Γ F, the first projection function Οβ: E Γ F β E is continuously differentiable of order n on s for all natural numbers n and infinitely differentiable.
|
ContDiffOn.add
theorem ContDiffOn.add :
β {π : 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] {n : ββ}
{s : Set E} {f g : E β F}, ContDiffOn π n f s β ContDiffOn π n g s β ContDiffOn π n (fun x => f x + g x) s
The theorem `ContDiffOn.add` states that for arbitrary types `π`, `E`, and `F` where `π` is a field with a nontrivial norm, `E` and `F` are normed additive commutative groups and are also normed spaces over `π`, if we have two functions `f` and `g` from `E` to `F` that are continuously differentiable of any order `n` (possibly infinity) on a set `s` in `E`, then the function that maps each element `x` in `E` to the sum of `f(x)` and `g(x)` is also continuously differentiable of the same order `n` on the same set `s`. This theorem captures one of the basic properties of differentiable functions, namely, that the sum of two differentiable functions is again differentiable, with the derivative of the sum being the sum of the derivatives.
More concisely: If `f` and `g` are continuously differentiable of order `n` from a set `s` in the normed additive commutative groups and normed spaces `E` and `F` over a field `π` with a nontrivial norm, then their sum `f + g` is also continuously differentiable of order `n` on `s`.
|
contDiff_neg
theorem contDiff_neg :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {n : ββ}, ContDiff π n fun p => -p
This theorem states that for any nontrivially normed field `π` and any normed additive commutative group `F` that also forms a normed space over `π`, the negation function (which maps each point `p` to its negation `-p`) is continuously differentiable of any order `n`, where `n` can be any natural number or infinity (`ββ`). Thus, the negative of any point in this normed space is smooth, meaning it has derivatives of all orders.
More concisely: For any nontrivially normed field `π` and normed additive commutative group `F` over `π` that is also a normed space, the negation function `- : F β F` is continuously differentiable of any order `n` (`n : ββ`).
|
contDiffOn_top_iff_derivWithin
theorem contDiffOn_top_iff_derivWithin :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F} {sβ : Set π},
UniqueDiffOn π sβ β (ContDiffOn π β€ fβ sβ β DifferentiableOn π fβ sβ β§ ContDiffOn π β€ (derivWithin fβ sβ) sβ)
The theorem `contDiffOn_top_iff_derivWithin` states that for any nontrivially normed field `π`, any normed additive commutative group `F` that is also a normed space over `π`, any function `fβ` from `π` to `F`, and any set `sβ` of `π`, assuming that `sβ` has unique derivatives, the function `fβ` is infinitely continuously differentiable on `sβ` if and only if `fβ` is differentiable on `sβ` and the derivative of `fβ` (formulated with `derivWithin`) is also infinitely continuously differentiable on `sβ`. Here, continuous differentiability of order `β€` means that the function is differentiable and its derivatives of all orders exist and are continuous.
More concisely: A function from a nontrivially normed field to a normed space over that field, with unique derivatives on a set, is infinitely continuously differentiable on that set if and only if it is differentiable and its derivative is also infinitely continuously differentiable on that set.
|
ContDiffWithinAt.pow
theorem ContDiffWithinAt.pow :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E} {n : ββ} {πΈ : Type u_3} [inst_3 : NormedRing πΈ]
[inst_4 : NormedAlgebra π πΈ] {f : E β πΈ},
ContDiffWithinAt π n f s x β β (m : β), ContDiffWithinAt π n (fun y => f y ^ m) s x
The theorem `ContDiffWithinAt.pow` states the following: For any nontrivially normed field `π`, any normed add commutative group `E` that is a normed space over `π`, any set `s` of elements of `E`, any element `x` of `E`, any `ββ` number `n`, any normed ring `πΈ` that is a normed algebra over `π`, and any function `f` from `E` to `πΈ`, if the function `f` is continuously differentiable within the set `s` at the point `x` to the `n`-th degree, then for any natural number `m`, the function `(fun y => f y ^ m)` which raises `f y` to the `m`-th power, is also continuously differentiable within the set `s` at the point `x` to the `n`-th degree.
More concisely: If a function is continuously differentiable within a set to a certain degree at a point in a normed space over a nontrivially normed field, then the function composed with raising to a constant power is also continuously differentiable within the set to the same degree at the point.
|
ContDiff.fst'
theorem ContDiff.fst' :
β {π : 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] {n : ββ} {f : E β G},
ContDiff π n f β ContDiff π n fun x => f x.1
This theorem states that for any nontrivially normed field `π`, and normed additive commutative groups `E`, `F`, and `G` over `π`, given a function `f` from `E` to `G`, if `f` is `C^n` continuous differentiable, then the function that takes a pair `(x, y)` in `E Γ F` and returns `f(x)`, which is the composition of `f` with the projection onto the first factor `Prod.fst`, is also `C^n` continuous differentiable.
More concisely: If `f` is a `C^n` continuous differentiable function from a normed additive commutative group `E` to another normed additive commutative group `G` over a nontrivially normed field `π`, then the function `x => f(x)` from `E Γ G` to `G`, obtained by composing `f` with the projection onto the first factor, is also `C^n` continuous differentiable.
|
ContDiff.snd
theorem ContDiff.snd :
β {π : 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] {n : ββ} {f : E β F Γ G},
ContDiff π n f β ContDiff π n fun x => (f x).2
This theorem, `ContDiff.snd`, states that for any nontrivially normed field `π`, normed additive commutative groups `E`, `F`, and `G`, which are also normed spaces over `π`, and for any function `f` mapping from `E` to a pair in `F Γ G`, if `f` is `C^n` continuous differentiable, then the function that maps `x` from `E` to the second component of `f(x)` is also `C^n` continuous differentiable. Here, `C^n` refers to the class of functions that can be differentiated `n` times with a result that is still continuous. This theorem essentially asserts the continuous differentiability of the function obtained by postcomposing `f` with `Prod.snd`, which retrieves the second component of a pair.
More concisely: If `f: E β F Γ G` is a `C^n` differentiable function between two normed spaces over a nontrivially normed field, then the function `g(x) = f(x).2` mapping `x` from `E` to the second component of `f(x)` is also `C^n` differentiable.
|
Mathlib.Analysis.Calculus.ContDiff.Basic._auxLemma.8
theorem Mathlib.Analysis.Calculus.ContDiff.Basic._auxLemma.8 :
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F}
{n : ββ}, ContDiff π n f = ContDiffOn π n f Set.univ
This theorem states that for any type `π` which forms a nontrivially normed field, types `E` and `F` which both form normed additive commutative groups and normed spaces over `π`, a function `f` from `E` to `F`, and a natural number or infinity `n`, the function `f` is continuously differentiable to degree `n` across the entire space if and only if it is continuously differentiable to degree `n` on the universal set `Set.univ` of `E` (which includes all elements of `E`). In other words, the function `f` is continuously differentiable everywhere.
More concisely: For any normed field `π`, normed additive commutative groups and normed spaces `E` and `F` over `π`, and a continuously differentiable function `f` from `E` to `F` of degree `n`, `f` is continuously differentiable to degree `n` everywhere if and only if it is continuously differentiable to degree `n` on the universal set of `E`.
|
ContDiffOn.prod_map
theorem ContDiffOn.prod_map :
β {π : 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] {n : ββ}
{E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace π E'] {F' : Type u_6}
[inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace π F'] {s : Set E} {t : Set E'} {f : E β F} {g : E' β F'},
ContDiffOn π n f s β ContDiffOn π n g t β ContDiffOn π n (Prod.map f g) (s ΓΛ’ t)
The theorem `ContDiffOn.prod_map` states that, given two functions `f` and `g` that are `n` times continuously differentiable on sets `s` and `t` respectively, the product map of `f` and `g` (formed by applying `f` to the first component of a pair and `g` to the second) is also `n` times continuously differentiable on the Cartesian product of sets `s` and `t`.
This holds for any types `π`, `E`, `F`, `E'`, `F'` where `π` is a nontrivial normed field, `E` and `E'` are normed additive commutative groups over `π` with a normed space structure, and `F` and `F'` are also normed additive commutative groups over `π` with a normed space structure. The smoothness level `n` is an element of `ββ`, the set of natural numbers including infinity.
More concisely: Given two `n` times continuously differentiable functions `f` and `g` over normed fields `π` with values in normed spaces `E` and `F` respectively, their product `h(x, y) = (f(x), g(y))` is also `n` times continuously differentiable over the Cartesian product of their domains.
|
ContDiffAt.prod_map'
theorem ContDiffAt.prod_map' :
β {π : 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] {n : ββ}
{E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace π E'] {F' : Type u_4}
[inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace π F'] {f : E β F} {g : E' β F'} {p : E Γ E'},
ContDiffAt π n f p.1 β ContDiffAt π n g p.2 β ContDiffAt π n (Prod.map f g) p
The given theorem asserts that if two functions `f` and `g`, which map from types `E` to `F` and `E'` to `F'` respectively, are both continuously differentiable of order `n` at points `p.1` and `p.2` respectively, then the product map of these two functions, which maps from `E Γ E'` to `F Γ F'`, is also continuously differentiable of the same order `n` at the corresponding product point `p`. Here, `π` is a non-trivial normed field and `E`, `F`, `E'`, `F'` are normed spaces over `π`. This theorem essentially speaks about the preservation of continuous differentiability when mapping across pairs using two continuously differentiable functions.
More concisely: If functions `f : E -> F` and `g : E' -> F'` are continuously differentiable of order `n` at points `p.1 in E` and `p.2 in E'`, respectively, then their product function `f β g : E Γ E' -> F Γ F'` is also continuously differentiable of order `n` at the product point `(p.1, p.2)`.
|
ContDiffWithinAt.add
theorem ContDiffWithinAt.add :
β {π : 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] {x : E}
{n : ββ} {s : Set E} {f g : E β F},
ContDiffWithinAt π n f s x β ContDiffWithinAt π n g s x β ContDiffWithinAt π n (fun x => f x + g x) s x
This theorem asserts that the sum of two functions, each of which is continuously differentiable to order `n` within a set `s` at a point `x`, is also continuously differentiable to order `n` at that point within the same set. Here, the underlying field is a nontrivial normed field `π`, and the functions `f` and `g` both map from a normed additive commutative group `E`, which is also a normed space over the field `π`, to another normed additive commutative group `F`, which is also a normed space over the field `π`. The smoothness order `n` can be a natural number or infinity (`ββ`).
More concisely: If `f` and `g` are continuously differentiable to order `n` at `x` in the normed spaces `E` and `F` over the nontrivial normed field `π`, then their sum `f + g` is also continuously differentiable to order `n` at `x`.
|
ContDiff.add
theorem ContDiff.add :
β {π : 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] {n : ββ}
{f g : E β F}, ContDiff π n f β ContDiff π n g β ContDiff π n fun x => f x + g x
This theorem states that given two functions `f` and `g` that are `C^n` (i.e., continuously differentiable n times) from a normed space `E` to a normed space `F` over a nontrivially normed field `π`, the sum of these two functions is also `C^n`. In other words, the sum of two continuously differentiable functions is also continuously differentiable.
More concisely: Given two `C^n` functions `f : E -> F` and `g : E -> F` from a normed space `E` to a normed space `F` over a nontrivially normed field `π`, their sum `f + g : E -> F` is also a `C^n` function.
|
ContDiffWithinAt.fderivWithin''
theorem ContDiffWithinAt.fderivWithin'' :
β {π : 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] {s : Set E} {xβ : E} {m : ββ} {f : E β F β G}
{g : E β F} {t : Set F} {n : ββ},
ContDiffWithinAt π n (Function.uncurry f) (insert xβ s ΓΛ’ t) (xβ, g xβ) β
ContDiffWithinAt π m g s xβ β
(βαΆ (x : E) in nhdsWithin xβ (insert xβ s), UniqueDiffWithinAt π t (g x)) β
m + 1 β€ n β
t β nhdsWithin (g xβ) (g '' s) β ContDiffWithinAt π m (fun x => fderivWithin π (f x) t (g x)) s xβ
This theorem, `ContDiffWithinAt.fderivWithin''`, establishes conditions under which the function `x β¦ fderivWithin π (f x) t (g x)` is continuously differentiable of an arbitrary order `m` at a given point `xβ` within a set `s`. Specifically, the theorem states that if the following conditions are met:
1. The function `f` is continuously differentiable of order `n` (where `n β₯ m+1`) at the point `(xβ, g(xβ))` within the product set `(s βͺ {xβ}) Γ t`.
2. The function `g` is continuously differentiable of order `m` at the point `xβ` within the set `s`.
3. The derivative of the function `f` is unique at each point `g(x)` within the set `t` for all `x` sufficiently close to `xβ` within the set `s βͺ {xβ}`. This condition must be met eventually in the neighborhood of `xβ` within `s βͺ {xβ}`.
4. The set `t` is a neighborhood of `g(xβ)` within the image of `s` under `g`.
Then the function `x β¦ fderivWithin π (f x) t (g x)` is continuously differentiable of order `m` at the point `xβ` within the set `s`. This statement is a generalization of the chain rule in calculus to arbitrary orders of differentiation and to functions defined on subsets of their domain.
More concisely: If `f` is continuously differentiable of order `n (n >= m+1)` at `(xβ, g(xβ))` within the product set `(s βͺ {xβ}) Γ t`, `g` is continuously differentiable of order `m` at `xβ` within `s`, and the derivative of `f` is unique at each `g(x)` within `t` for all `x` sufficiently close to `xβ` within `s βͺ {xβ}`, then the function `x β¦ fderivWithin π (f x) t (g x)` is continuously differentiable of order `m` at `xβ` within `s`.
|
IsBoundedLinearMap.contDiff
theorem IsBoundedLinearMap.contDiff :
β {π : 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] {f : E β F}
{n : ββ}, IsBoundedLinearMap π f β ContDiff π n f
This theorem states that for any unbundled bounded linear map `f` from a normed additive commutative group `E` over a non-trivially normed field `π` to another normed additive commutative group `F` over the same field, the map `f` is infinitely differentiable (`C^β`). In more technical terms, if `f` is a bounded linear map, then `f` is continuously differentiable any number of times (`n`), where `n` can even be infinite (`ββ`).
More concisely: A bounded linear map between two normed additive commutative groups over a non-trivially normed field is infinitely differentiable.
|
ContDiff.prod_map
theorem ContDiff.prod_map :
β {π : 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] {n : ββ}
{E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace π E'] {F' : Type u_4}
[inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace π F'] {f : E β F} {g : E' β F'},
ContDiff π n f β ContDiff π n g β ContDiff π n (Prod.map f g)
The theorem `ContDiff.prod_map` states that if you have two functions `f` and `g` that are `C^n` (i.e., n-times continuously differentiable) on their respective normed vector spaces, then the product map of `f` and `g` (which applies `f` to the first component of a pair and `g` to the second component) is also `C^n`. This theorem applies for any nontrivially normed field `π`, and it holds for any natural number `n` including infinity.
More concisely: If `f` and `g` are `C^n` functions on normed vector spaces, then their product function, which applies `f` to the first component and `g` to the second, is also `C^n`.
|
ContDiffAt.sub
theorem ContDiffAt.sub :
β {π : 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] {x : E}
{n : ββ} {f g : E β F}, ContDiffAt π n f x β ContDiffAt π n g x β ContDiffAt π n (fun x => f x - g x) x
This theorem states that for any two functions `f` and `g` which are continuously differentiable of order `n` at a given point `x` in a normed additive commutative group `E` with a normed space over a nontrivially normed field `π`, the difference of these two functions, `(f - g)`, is also continuously differentiable of the same order `n` at the point `x`. This is stated in the context of function spaces `F` which are also normed additive commutative groups with a normed space over the same nontrivially normed field `π`.
More concisely: If `f` and `g` are continuously differentiable of order `n` at point `x` in the normed additive commutative group `E` over the nontrivially normed field `π`, then their difference `(f - g)` is also continuously differentiable of order `n` at point `x`.
|
iteratedFDeriv_zero_fun
theorem iteratedFDeriv_zero_fun :
β {π : 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] {n : β},
(iteratedFDeriv π n fun x => 0) = 0
This theorem states that for any nontrivial normed field `π`, normed add commutative group `E`, normed space of `π` and `E`, another normed add commutative group `F`, another normed space of `π` and `F`, and a natural number `n`, the `n`-th iterated Frechet derivative of the zero function (i.e., a function that always returns zero) is also zero. This is essentially saying that if you take any number of derivatives of a constant zero function, you'll always get zero, regardless of the spaces and fields involved.
More concisely: The `n`-th Frechet derivative of the zero function is zero for any normed field, normed add commutative group, and natural number.
|
ContDiffWithinAt.hasFDerivWithinAt_nhds
theorem ContDiffWithinAt.hasFDerivWithinAt_nhds :
β {π : 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] {s : Set E} {f : E β F β G} {g : E β F} {t : Set F}
{n : β} {xβ : E},
ContDiffWithinAt π (βn + 1) (Function.uncurry f) (insert xβ s ΓΛ’ t) (xβ, g xβ) β
ContDiffWithinAt π (βn) g s xβ β
t β nhdsWithin (g xβ) (g '' s) β
β v β nhdsWithin xβ (insert xβ s),
v β insert xβ s β§
β f',
(β x β v, HasFDerivWithinAt (f x) (f' x) t (g x)) β§ ContDiffWithinAt π (βn) (fun x => f' x) s xβ
The theorem `ContDiffWithinAt.hasFDerivWithinAt_nhds` states that for a certain class of functions and under certain conditions, if `f : E Γ F β G` is continuously differentiable of order `n+1` at the pair `(xβ, g(xβ))` within the set `(s βͺ {xβ}) Γ t β E Γ F`, and a function `g : E β F` is continuously differentiable of order `n` at `xβ` within a set `s β E`, then there exists a function `f' : E β F βL[π] G` that is continuously differentiable of order `n` at `xβ` within `s` such that for all `x` sufficiently close to `xβ` within `s βͺ {xβ}`, the function `y β¦ f x y` has derivative `f' x` at `g x` within `t β F`. Additionally, the theorem states that the set `t` is a neighborhood of `g(xβ)` within `g '' s`. An explicit subset `v` of `s βͺ {xβ}` is also returned where this condition holds. This theorem is significant in the study of functions with parameters and their derivatives, in particular, it deals with the continuity of the derivative function in relation to the original function.
More concisely: Given a continuously differentiable function `f : E Γ F β G` of order `n+1` at `(xβ, g(xβ))` within `(s βͺ {xβ}) Γ t` and a continuously differentiable function `g : E β F` of order `n` at `xβ` within `s`, there exists a continuously differentiable function `f' : E β F βL[π] G` of order `n` at `xβ` within `s` such that for all `x` close to `xβ` within `s βͺ {xβ}`, the derivative of `y β¦ f x y` at `g x` exists within `t` and equals `f' x`. The set `t` is a neighborhood of `g(xβ)` within `g '' s`.
|
ContDiff.mul
theorem ContDiff.mul :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ} {πΈ : Type u_3} [inst_3 : NormedRing πΈ] [inst_4 : NormedAlgebra π πΈ]
{f g : E β πΈ}, ContDiff π n f β ContDiff π n g β ContDiff π n fun x => f x * g x
The theorem `ContDiff.mul` states that if we have two functions `f` and `g` from a normed space `E` over a non-trivially normed field `π` to a normed ring `πΈ`, which is also a normed algebra over `π`, and if both these functions are `C^n` (i.e., continuously differentiable up to the `n`th derivative), then the product function `(x => f x * g x)` is also `C^n`.
More concisely: If two `C^n` functions from a normed space to a normed algebra over a non-trivially normed field satisfy the commutative multiplication property, then their product is also a `C^n` function.
|
ContDiffAt.comp_contDiffWithinAt
theorem ContDiffAt.comp_contDiffWithinAt :
β {π : 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] {s : Set E} {f : E β F} {g : F β G} {n : ββ} (x : E),
ContDiffAt π n g (f x) β ContDiffWithinAt π n f s x β ContDiffWithinAt π n (g β f) s x
The theorem `ContDiffAt.comp_contDiffWithinAt` states that for dependent types π, E, F, and G, where π is a non-trivial normed field and E, F, G are normed spaces over π, given a set `s` of elements of type E, and two functions `f` and `g` with type E β F and F β G respectively, if `g` is continuously differentiable at the point `f(x)` and `f` is continuously differentiable within the set `s` at the point `x`, then the composition of `g` and `f` is continuously differentiable within the set `s` at the point `x`. This theorem is a statement about the compatibility of continuous differentiability with function composition in the settings of normed spaces over a non-trivial normed field.
More concisely: If `f` is continuously differentiable within a set `s` at `x` in a normed space over a non-trivial normed field, and `g` is continuously differentiable at `f(x)`, then the composition `g β f` is continuously differentiable at `x`.
|
ContDiff.smul
theorem ContDiff.smul :
β {π : 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] {n : ββ}
{f : E β π} {g : E β F}, ContDiff π n f β ContDiff π n g β ContDiff π n fun x => f x β’ g x
This theorem states that given two functions `f` and `g` from a normed additive commutative group `E` to a normed field `π` and a normed additive commutative group `F` respectively, if both functions are continuously differentiable of order `n`, then the function obtained by multiplying the scalar output of `f` with the output of `g` is also continuously differentiable of order `n`. This holds under the assumption that `π` is a nontrivially normed field and both `E` and `F` are normed spaces over `π`.
More concisely: Given two continuously differentiable functions of order `n` from a normed additive commutative group to a nontrivially normed field, their pointwise product is also continuously differentiable of order `n`.
|
ContDiffWithinAt.const_smul
theorem ContDiffWithinAt.const_smul :
β {π : 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] {n : ββ}
{R : Type u_3} [inst_5 : Semiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass π R F]
[inst_8 : ContinuousConstSMul R F] {s : Set E} {f : E β F} {x : E} (c : R),
ContDiffWithinAt π n f s x β ContDiffWithinAt π n (fun y => c β’ f y) s x
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E` and `F`, normed spaces `E` and `F` over `π`, a semiring `R`, a module `F` over `R`, a commutative multiplication operation between `π` and `R`, continuous scalar multiplication of `R` and `F`, a set `s` of elements from `E`, a function `f` mapping `E` to `F`, and a point `x` in `E`, if the function `f` is `n` times continuously differentiable within the set `s` at the point `x`, then the function obtained by scalar multiplication of the function `f` by a constant `c` from `R` is also `n` times continuously differentiable within the set `s` at the point `x`. In mathematical terms, if `f` is `C^n` within a set at a point, then `c*f` is also `C^n` at the same point within the same set.
More concisely: If `f: E β F` is `C^n` at `x β E` with respect to a normed field `π`, then the function `c β¦ c * f` is also `C^n` at `x` for any constant `c` in a commutative semiring `R` with continuous scalar multiplication on `F`.
|
contDiff_pi
theorem contDiff_pi :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {n : ββ} {ΞΉ : Type u_3} [inst_3 : Fintype ΞΉ] {F' : ΞΉ β Type u_5}
[inst_4 : (i : ΞΉ) β NormedAddCommGroup (F' i)] [inst_5 : (i : ΞΉ) β NormedSpace π (F' i)] {Ξ¦ : E β (i : ΞΉ) β F' i},
ContDiff π n Ξ¦ β β (i : ΞΉ), ContDiff π n fun x => Ξ¦ x i
The theorem `contDiff_pi` states that for any non-trivially normed field `π`, normed additive commutative group `E`, normed space `π E`, a function `Ξ¦ : E β (i : ΞΉ) β F' i` where `F' : ΞΉ β Type u_5` is a normed additive commutative group and normed space `π (F' i)` for each `i : ΞΉ`, the function `Ξ¦` is continuously differentiable of any order `n` if and only if for each `i : ΞΉ`, the function `fun x => Ξ¦ x i` is continuously differentiable of order `n`. In other words, a function between normed spaces is continuously differentiable of a certain order if and only if each of its component functions is.
More concisely: A function `Ξ¦ : E β (i : ΞΉ) β F' i` between normed spaces is continuously differentiable of order `n` if and only if each component function `fun x => Ξ¦ x i` is.
|
contDiff_top_iff_deriv
theorem contDiff_top_iff_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {F : Type uF} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace π F] {fβ : π β F}, ContDiff π β€ fβ β Differentiable π fβ β§ ContDiff π β€ (deriv fβ)
The theorem `contDiff_top_iff_deriv` states that a function `fβ` is infinitely differentiable (denoted as `C^β`) over a non-trivially normed field `π` if and only if it is differentiable and its derivative (expressed in terms of the function `deriv`) is also infinitely differentiable. Here, `Differentiable π fβ` means that the function `fβ` is differentiable at any point in the domain `π`. The `deriv` function calculates the derivative of `fβ` at a given point, giving zero if the derivative does not exist. Infinitely differentiable functions (or `C^β` functions) are functions that have derivatives of all degrees.
More concisely: A function `fβ` over a non-trivially normed field `π` is infinitely differentiable if and only if it is differentiable and its derivative is also infinitely differentiable.
|
ContDiffAt.prod_map
theorem ContDiffAt.prod_map :
β {π : 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] {n : ββ}
{E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace π E'] {F' : Type u_4}
[inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace π F'] {f : E β F} {g : E' β F'} {x : E} {y : E'},
ContDiffAt π n f x β ContDiffAt π n g y β ContDiffAt π n (Prod.map f g) (x, y)
The theorem `ContDiffAt.prod_map` states that, for any non-trivially normed field `π`, two normed add commutative groups `E` and `F` and two more normed add commutative groups `E'` and `F'`, all with the normed space over `π`, a point `x` in `E`, a point `y` in `E'`, and two functions `f` from `E` to `F` and `g` from `E'` to `F'`, if the functions `f` and `g` are `n`-times continuously differentiable at the points `x` and `y` respectively, then the product map of `f` and `g` is also `n`-times continuously differentiable at the pair `(x, y)`. In mathematical terms, we say that if `f` is `C^n` at `x` and `g` is `C^n` at `y`, then the product map `(f, g)` is `C^n` at `(x, y)`.
More concisely: If functions $f:\ E \to F$ and $g:\ E' \to F'$ are $C^n$ at points $x \in E$ and $y \in E'$, respectively, then their product $(f, g):\ (E, E') \to (F, F')$ is $C^n$ at the pair $(x, y)$.
|
contDiffAt_snd
theorem contDiffAt_snd :
β {π : 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] {n : ββ}
{p : E Γ F}, ContDiffAt π n Prod.snd p
This theorem states that for any point `p` in the Cartesian product of two normed vector spaces `E` and `F` over a nontrivially normed field `π`, the function that projects onto the second component (from the pair `p` to the second element of the pair) is `C^β`, or infinitely continuously differentiable. In other words, the second projection function is smooth at any point in the Cartesian product of these two spaces.
More concisely: The second projection function on the Cartesian product of two normed vector spaces over a nontrivially normed field is infinitely differentiable.
|
IsBoundedBilinearMap.contDiff
theorem IsBoundedBilinearMap.contDiff :
β {π : 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] {b : E Γ F β G} {n : ββ},
IsBoundedBilinearMap π b β ContDiff π n b
This theorem states that for any non-trivial normed field π, if `b` is a bounded bilinear map from a product of two normed spaces (E, F) over π to another normed space G over π, then `b` is continuously differentiable of any order `n`. In simpler terms, the theorem asserts that all bounded bilinear maps are infinitely differentiable.
More concisely: For any non-trivial normed field π, every bounded bilinear map from the product of two normed spaces over π to another normed space over π is infinitely differentiable.
|
contDiffWithinAt_prod'
theorem contDiffWithinAt_prod' :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {s : Set E} {x : E} {n : ββ} {πΈ' : Type u_4} {ΞΉ : Type u_5}
[inst_3 : NormedCommRing πΈ'] [inst_4 : NormedAlgebra π πΈ'] {t : Finset ΞΉ} {f : ΞΉ β E β πΈ'},
(β i β t, ContDiffWithinAt π n (f i) s x) β ContDiffWithinAt π n (t.prod fun i => f i) s x
The theorem `contDiffWithinAt_prod'` states that for any nontrivially normed field `π`, a normed additive commutative group `E` over `π`, a set `s` of elements of `E`, an element `x` in `E`, a natural number `n` (possibly infinity), a normed commutative ring `πΈ'` over `π`, a finite set `t` of elements of some type `ΞΉ`, and a function `f` mapping each element of `ΞΉ` to a function from `E` to `πΈ'`, if each function `f i` is continuously differentiable within `s` at `x` to order `n` for every `i` in `t`, then the product of all the functions `f i` (i.e., `Finset.prod t fun i => f i`) is also continuously differentiable within `s` at `x` to order `n`.
In mathematical terms, if `$f_i : E \to πΈ'$` is continuously differentiable to order `n` within a set `s` at a point `x` for all `i` in a finite set `t`, then the product of the `$f_i$`'s is also continuously differentiable to the same order within `s` at `x`.
More concisely: If each function in a finite set of continuously differentiable functions from a normed additive commutative group to a normed commutative ring is continuously differentiable within a set to order n at a point, then their product is also continuously differentiable to the same order within that set at that point.
|
ContDiff.contDiff_fderiv_apply
theorem ContDiff.contDiff_fderiv_apply :
β {π : 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] {m n : ββ}
{f : E β F}, ContDiff π n f β m + 1 β€ n β ContDiff π m fun p => (fderiv π f p.1) p.2
The theorem `ContDiff.contDiff_fderiv_apply` states that for any nontrivially normed field `π` and normed vector spaces `E` and `F` over `π`, if a function `f` from `E` to `F` is continuously differentiable up to order `n`, then the derivative of `f` considered as a map from `E` to the space of linear maps from `E` to `F`, is continuously differentiable up to order `m` provided that `m + 1` is less than or equal to `n`.
More concisely: If `f` is a continuously differentiable function of order `n` from a normed vector space `E` to a normed vector space `F` over a nontrivially normed field `π`, then the derivative of `f` as a map from `E` to the space of linear maps from `E` to `F` is continuously differentiable up to order `m` when `m + 1` is less than `n`.
|
ContDiff.div_const
theorem ContDiff.div_const :
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace π E] {π' : Type u_6} [inst_3 : NormedField π'] [inst_4 : NormedAlgebra π π'] {f : E β π'}
{n : ββ}, ContDiff π n f β β (c : π'), ContDiff π n fun x => f x / c
This theorem states that for any nontrivial normed field π, normed additive commutative group E, and normed space E over π, given a normed field π' and a normed algebra π' over π, if a function f from E to π' is continuously differentiable of any order n, then the function that applies f to an input and then divides by a fixed constant from π' is also continuously differentiable of the same order.
More concisely: If `f` is a continuously differentiable function of order `n` from a normed space `E` over a nontrivial normed field `β`, to another normed field `β'`, then the function `x β¦ (f(x) / k)` for a fixed `k` in `β'`, is also continuously differentiable of order `n`.
|
ContDiffOn.comp'
theorem ContDiffOn.comp' :
β {π : 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] {n : ββ} {s : Set E} {t : Set F} {g : F β G}
{f : E β F}, ContDiffOn π n g t β ContDiffOn π n f s β ContDiffOn π n (g β f) (s β© f β»ΒΉ' t)
The theorem `ContDiffOn.comp'` states that for any nontrivially normed field `π`, normed additive commutative groups `E`, `F`, `G` that also form normed spaces over `π`, and any two functions `f : E β F` and `g : F β G`, if `g` is `n` times continuously differentiable on a set `t` and `f` is `n` times continuously differentiable on a set `s`, then the composition of `g` and `f` (denoted by `g β f`) is also `n` times continuously differentiable on the intersection of `s` and the preimage of `t` under `f` (denoted by `s β© f β»ΒΉ' t`). In mathematical terms, this is saying that the composition of `C^n` functions is itself a `C^n` function.
More concisely: If functions `f : E β F` and `g : F β G` are `n` times continuously differentiable on sets `s` and `t`, respectively, then their composition `g β f` is `n` times continuously differentiable on the intersection of `s` and the preimage of `t` under `f`.
|
ContinuousLinearEquiv.contDiff_comp_iff
theorem ContinuousLinearEquiv.contDiff_comp_iff :
β {π : 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] {f : E β F} {n : ββ} (e : G βL[π] E),
ContDiff π n (f β βe) β ContDiff π n f
This theorem states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` which are also normed spaces over `π`, a function `f : E β F`, a natural number or infinity `n`, and a continuous linear equivalence `e : G βL[π] E`, the function `f` composed with the inverse of `e` is `n`-times continuously differentiable if and only if `f` itself is `n`-times continuously differentiable. This essentially means that differentiability is preserved under composition with a continuous linear equivalence.
More concisely: For any non-trivially normed field `π`, if `f : E β F` is `n`-times continuously differentiable between normed spaces `E` and `F` over `π`, and `e : G βL[π] E` is a continuous linear equivalence, then `f β eβ»ΒΉ` is also `n`-times continuously differentiable.
|
ContDiffWithinAt.comp'
theorem ContDiffWithinAt.comp' :
β {π : 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] {n : ββ} {s : Set E} {t : Set F} {g : F β G}
{f : E β F} (x : E),
ContDiffWithinAt π n g t (f x) β ContDiffWithinAt π n f s x β ContDiffWithinAt π n (g β f) (s β© f β»ΒΉ' t) x
The theorem `ContDiffWithinAt.comp'` states that for any non-trivially normed field `π`, normed add commutative groups `E`, `F`, and `G` that are also normed spaces over `π`, and any set of elements of type `E` (`s`) and `F` (`t`), if the function `g` mapping `F` to `G` is continuously differentiable of order `n` within the set `t` at the point `f(x)`, and the function `f` mapping `E` to `F` is continuously differentiable of order `n` within the set `s` at the point `x`, then the composition of functions `g β f` is also continuously differentiable of order `n` within the intersection of the set `s` and the preimage of the set `t` under the function `f`, at the point `x`.
More concisely: If functions `f: E β F` and `g: F β G` are continuously differentiable of order `n` at a point `x in E` and `f(x) in T`, respectively, then the composition `g β f` is continuously differentiable of order `n` at `x` when `x` is in the intersection of `S` and `f^(-1)(T)`.
|
ContDiff.fderiv
theorem ContDiff.fderiv :
β {π : 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] {f : E β F β G} {g : E β F} {n m : ββ},
ContDiff π m (Function.uncurry f) β ContDiff π n g β n + 1 β€ m β ContDiff π n fun x => fderiv π (f x) (g x)
The theorem `ContDiff.fderiv` establishes that the function `x β¦ fderiv π (f x) (g x)` is smooth under certain conditions. More specifically, if `f` is a function from `E` to `F β G` and `g` is a function from `E` to `F`, both of which are differentiable up to certain orders `m` and `n` respectively over the nontrivially normed field `π`, and `n + 1 β€ m`, then the function that maps `x` to the derivative of `(f x)` at `(g x)` is `n`-times continuously differentiable. This means that we can differentiate this function `n` times and the result will still be a continuous function.
More concisely: If `f : E β F β G` is `(m+1)`-times differentiable and `g : E β F` is `n`-times differentiable over the nontrivially normed field `π` with `n+1 β€ m`, then the function `x β¦ fderiv π (f x) (g x)` is `n`-times continuously differentiable.
|
ContDiffAt.comp
theorem ContDiffAt.comp :
β {π : 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] {f : E β F} {g : F β G} {n : ββ} (x : E),
ContDiffAt π n g (f x) β ContDiffAt π n f x β ContDiffAt π n (g β f) x
This theorem states that if we have two functions, `f` and `g`, that are `C^n` differentiable at a given point `x`, then the composition of `g` and `f`, represented by `(g β f)`, is also `C^n` differentiable at the same point `x`. Here, `C^n` refers to a class of functions that are differentiable up to the `n`th derivative, `π` denotes a non-trivially normed field, `E`, `F`, and `G` are normed addition-commutative groups with a normed space structure over `π`, and `n` can be any natural number or infinity (`ββ`).
More concisely: If `f : E β F` and `g : F β G` are `C^n` differentiable functions at `x β E`, then `g β f` is `C^n` differentiable at `x`.
|
ContDiffAt.snd'
theorem ContDiffAt.snd' :
β {π : 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] {n : ββ} {f : F β G} {x : E} {y : F},
ContDiffAt π n f y β ContDiffAt π n (fun x => f x.2) (x, y)
This theorem states that for a given function `f` mapping from a normed additive commutative group `F` to another one `G`, if `f` is `C^n` differentiable at a point `y` in `F`, then the function that maps an ordered pair `(x, y)` to `f(y)` is also `C^n` differentiable at the same point `y`, regardless of the value of `x`. Here, `C^n` denotes the class of functions which have continuous derivatives up to order `n`. The normed additive commutative groups and the field `π` are over generic types `E`, `F`, `G` and `π` respectively, and they are equipped with the necessary algebraic structures.
More concisely: If `f : F -> G` is `C^n` differentiable at `y` in the normed additive commutative group `F`, then the function `x => f y` is also `C^n` differentiable at `y` in the variables `x` from `E`.
|
LinearIsometryEquiv.norm_iteratedFDeriv_comp_right
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right :
β {π : 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 : G ββα΅’[π] E) (f : E β F) (x : G) (i : β),
βiteratedFDeriv π i (f β βg) xβ = βiteratedFDeriv π i f (g x)β
This theorem states that for a given non-trivial normed field π, normed additive commutative groups E, F, and G, and their corresponding normed spaces over π, if there exists a linear isometry 'g' mapping G to E, and a function 'f' mapping E to F, then for any element 'x' in G and a natural number 'i', the norm of the 'i'-th iterated FrΓ©chet derivative of the function 'f' composed with the inverse of 'g' at the point 'x' is equal to the norm of the 'i'-th iterated FrΓ©chet derivative of 'f' at the point 'g' of 'x'. In simpler terms, composing a function with a linear isometry on the right side preserves the norm of its iterated derivatives within a set.
More concisely: For a normed field π, normed additive commutative groups E, F, and G, and linear isometry g: G β E, if there exists a function f: E β F, then the norm of the i-th iterated Frechet derivative of f β g^-1 at x in G equals the norm of the i-th iterated Frechet derivative of f at g(x) in F.
|
contDiffAt_ring_inverse
theorem contDiffAt_ring_inverse :
β (π : Type u_1) [inst : NontriviallyNormedField π] {n : ββ} {R : Type u_3} [inst_1 : NormedRing R]
[inst_2 : NormedAlgebra π R] [inst_3 : CompleteSpace R] (x : RΛ£), ContDiffAt π n Ring.inverse βx
This theorem states that in a complete normed algebra, the function of inversion, which sends each invertible element to its inverse, is `C^n` for all `n` at each invertible element. `C^n` refers to the class of functions that are continuously differentiable `n` times. Here, the normed algebra is over a non-trivially normed field `π` and the ring `R`. The theorem holds for each invertible element `x` in `R`. The proof of this theorem involves an induction, and it uses an identity that expresses the derivative of inversion as a bilinear map of inversion itself.
More concisely: In a complete normed algebra over a non-trivially normed field, the function of inversion is continuously differentiable (C^\infty) at each invertible element.
|
ContDiff.prod
theorem ContDiff.prod :
β {π : 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] {n : ββ} {f : E β F} {g : E β G},
ContDiff π n f β ContDiff π n g β ContDiff π n fun x => (f x, g x)
The theorem `ContDiff.prod` states that for any non-trivially normed field `π`, normed additive commutative groups `E`, `F`, and `G` that are also normed spaces over `π`, and for any functions `f : E β F` and `g : E β G` that are n-times continuously differentiable, the cartesian product function `(f, g) : E β F Γ G` is also n-times continuously differentiable. The cartesian product function is defined by `(f, g)(x) = (f(x), g(x))` for every `x` in `E`.
More concisely: For any non-trivially normed fields `π` and normed additive commutative groups/normed spaces `E`, `F`, and `G` over `π`, if `f : E β F` and `g : E β G` are n-times continuously differentiable functions, then the cartesian product function `(f, g) : E β F Γ G` is also n-times continuously differentiable.
|
Homeomorph.contDiff_symm_deriv
theorem Homeomorph.contDiff_symm_deriv :
β {π : Type u_1} [inst : NontriviallyNormedField π] {n : ββ} [inst_1 : CompleteSpace π] (f : π ββ π) {f' : π β π},
(β (x : π), f' x β 0) β (β (x : π), HasDerivAt (βf) (f' x) x) β ContDiff π n βf β ContDiff π n βf.symm
The theorem `Homeomorph.contDiff_symm_deriv` states that if `f` is an `n` times continuously differentiable homeomorphism of a nontrivially normed field, and its derivative is never equal to zero, then the inverse of `f`, denoted `f.symm`, is also `n` times continuously differentiable. This theorem forms a part of the inverse function theorem, but assumes the existence of an inverse function. In the context of this theorem, π is a nontrivially normed field, `n` is a natural number or infinite, and `f` is a homeomorphism mapping π to π. The function `f` is differentiated `n` times continuously, and the theorem ensures that the inverse of `f`, `f.symm`, shares the same property.
More concisely: If `f` is an `n`-times continuously differentiable homeomorphism of a nontrivially normed field with non-zero derivative, then its inverse is also `n`-times continuously differentiable.
|
contDiffOn_const
theorem contDiffOn_const :
β {π : 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] {n : ββ}
{c : F} {s : Set E}, ContDiffOn π n (fun x => c) s
The theorem `contDiffOn_const` states that for any non-trivially normed field `π`, any normed additive commutative groups `E` and `F` that are also normed spaces over `π`, any natural number or infinity `n`, any constant `c` of type `F`, and any set `s` of elements of type `E`, the function that always returns `c` is continuously differentiable on the set `s`.
More concisely: For any non-trivially normed field π, any normed additive commutative groups E and F as normed spaces over π, any natural number or infinity n, any constant c in F, and any set s of elements in E, the constant function mapping x to c is continuously differentiable on s.
|
contDiffWithinAt_const
theorem contDiffWithinAt_const :
β {π : 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] {s : Set E}
{x : E} {n : ββ} {c : F}, ContDiffWithinAt π n (fun x => c) s x
The theorem `contDiffWithinAt_const` states that for any nontrivially normed field `π`, normed additive commutative group `E`, normed space over `π` and `E`, another normed additive commutative group `F`, another normed space over `π` and `F`, any set `s` of elements of type `E`, any element `x` of type `E`, any extended natural number `n`, and any element `c` of type `F`, the function that always returns `c` is continuously differentiable `n` times within the set `s` at the point `x`. In mathematical terms, it states that a constant function is continuously differentiable any number of times.
More concisely: A constant function is continuously differentiable of any order on any open set. (Note: In the context of the theorem description, "any open set" refers to the set `s` in the theorem statement.)
|