ContDiffWithinAt.contMDiffWithinAt
theorem ContDiffWithinAt.contMDiffWithinAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {s : Set E} {x : E},
ContDiffWithinAt 𝕜 n f s x → ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x
This theorem states that, given a nontrivially normed field `𝕜`, normed additive commutative groups `E` and `E'`, and normed spaces over `𝕜` for `E` and `E'`, for any function `f` from `E` to `E'`, any subset `s` of `E`, any point `x` in `E`, and any natural number or infinity `n`, if the function `f` is continuously differentiable within the set `s` at the point `x` up to order `n` over the field `𝕜`, then `f` is continuously differentiable within the set `s` at the point `x` up to order `n` in the manifold sense, using the trivial model with corners from `E` to `E` and from `E'` to `E'`.
More concisely: Given a nontrivially normed field `𝕜`, if a continuously differentiable function `f` from a normed additive commutative group `E` to another `E'` up to order `n` at a point `x` in `E` holds within a subset `s` of `E`, then `f` is continuously differentiable in the manifold sense up to order `n` from `E` to `E'` and from `E'` to `E'` using the trivial model with corners.
|
ContinuousLinearMap.contMDiff
theorem ContinuousLinearMap.contMDiff :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_8} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ∞}
(L : E →L[𝕜] F), ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n ⇑L
This theorem states that for any nontrivially normed field `𝕜`, given a continuous linear map `L` from a normed vector space `E` over `𝕜` to another normed vector space `F` over `𝕜`, the map `L` is continuously differentiable any number of times (`n` can be any natural number or infinity). The differentiability is checked in the context of the model with corners associated to the vector spaces `E` and `F`, which is the standard way to deal with differentiability in infinite-dimensional spaces.
More concisely: Given a continuous linear map between two normed vector spaces over a nontrivially normed field, it is infinitely differentiable.
|
ContDiff.contMDiff
theorem ContDiff.contMDiff :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'}, ContDiff 𝕜 n f → ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f
This theorem, named `ContDiff.contMDiff`, states that for any number `n` (which can be a natural number or infinity), and any function `f` from a normed space `E` to another normed space `E'` over a nontrivially normed field `𝕜`, if `f` is continuously differentiable up to order `n` over `𝕜`, then `f` is also continuously differentiable up to order `n` in the sense of manifold calculus on the model with corners built from `E` and `E'`. In other words, this theorem shows that the notion of continuous differentiability in the context of normed spaces extends naturally to the context of manifolds with corners.
More concisely: If `f` is continuously differentiable up to order `n` as a function from a normed space `E` to another normed space `E'` over a nontrivially normed field `𝕜`, then `f` is also continuously differentiable up to order `n` as a function on the manifolds with corners built from `E` and `E'`.
|
ContMDiffWithinAt.smul
theorem ContMDiffWithinAt.smul :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {n : ℕ∞}
{V : Type u_18} [inst_6 : NormedAddCommGroup V] [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 𝕜) n f s x →
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n g s x →
ContMDiffWithinAt I (modelWithCornersSelf 𝕜 V) n (fun p => f p • g p) s x
This theorem, `ContMDiffWithinAt.smul`, states that for every nontrivially normed field `𝕜`, normed additive commutative group `E` that forms a normed space over `𝕜`, a topological space `H`, a model with corners `I` from `𝕜` to `E` and `H`, a topological space `M` which is a charted space over `H`, a set `s` of `M`, a point `x` in `M`, possibly infinite natural number `n`, and a normed additive commutative group `V` that forms a normed space over `𝕜`, if a function `f` from `M` to `𝕜` is continuously differentiable within `s` at `x` up to order `n` and a function `g` from `M` to `V` is also continuously differentiable within `s` at `x` up to order `n`, then the function `p => f p • g p` is continuously differentiable within `s` at `x` up to order `n`. This theorem is a generalization of the product rule in differential calculus to the context of continuously differentiable manifolds.
More concisely: If functions `f` and `g` are continuously differentiable up to order `n` at a point `x` in a charted space `M` over a topological space `H`, then their product `p => f p • g p` is also continuously differentiable up to order `n` at `x`.
|
ContDiffAt.contMDiffAt
theorem ContDiffAt.contMDiffAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {x : E},
ContDiffAt 𝕜 n f x → ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x
This theorem, named `ContDiffAt.contMDiffAt`, is an alias of the reverse direction of `contMDiffAt_iff_contDiffAt`. It states that, given a non-trivially normed field `𝕜`, normed additive commutative groups `E` and `E'` and normed spaces over `𝕜` for `E` and `E'`, if a function `f` from `E` to `E'` is continuously differentiable at a point `x` in `E` at a certain smoothness level `n`, then the function `f` is also continuously differentiable in the manifold sense at the point `x` in `E` at the same smoothness level `n`, where the manifold is modeled with corners defined by `E` and `E'` themselves.
More concisely: If a function `f` from a normed space `E` to another normed space `E'` over a non-trivially normed field is `n`-times continuously differentiable at a point `x` in `E`, then `f` is also continuously differentiable in the manifold sense at `x` with manifolds `E` and `E'`.
|
ContMDiff.contDiff
theorem ContMDiff.contDiff :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'}, ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f → ContDiff 𝕜 n f
This theorem is an alias for the forward direction of `contMDiff_iff_contDiff`. It states that for any non-trivially normed field `𝕜`, normed add commutative groups `E` and `E'` which are also normed spaces over `𝕜`, and a function `f` from `E` to `E'`, if `f` is continuously differentiable with respect to the model with corners (or vector spaces) `E` and `E'` for any natural number `n`, then `f` is continuously differentiable in the standard sense for the same number `n`. In other words, if a function is smooth in the context of geometric structures, it is also smooth in the common sense.
More concisely: If a function between two normed spaces is continuously differentiable with respect to the model with corners, then it is continuously differentiable in the standard sense.
|
smooth_smul
theorem smooth_smul :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {V : Type u_18} [inst_1 : NormedAddCommGroup V]
[inst_2 : NormedSpace 𝕜 V],
Smooth ((modelWithCornersSelf 𝕜 𝕜).prod (modelWithCornersSelf 𝕜 V)) (modelWithCornersSelf 𝕜 V) fun p =>
p.1 • p.2
The theorem `smooth_smul` states that for any vector space, defined over a non-trivially normed field, the operation of scalar multiplication is smooth. More specifically, given any types `𝕜` and `V` such that `𝕜` is a non-trivially normed field, and `V` is a normed additive commutative group and a vector space over `𝕜`, the function that takes a pair `(p.1, p.2)` and maps it to the result of the scalar multiplication `p.1 • p.2` is smooth with respect to the model with corners structure on `𝕜` and `V`. This means that it has continuous derivatives of all orders.
More concisely: The scalar multiplication operation on a normed vector space over a non-trivially normed field is a smooth function.
|
ContMDiffOn.contDiffOn
theorem ContMDiffOn.contDiffOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {s : Set E},
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s → ContDiffOn 𝕜 n f s
The theorem `ContMDiffOn.contDiffOn` states that for all normed fields `𝕜`, normed additive commutative groups `E` and `E'`, and natural numbers or infinity `n`, if a function `f` from `E` to `E'` is continuously differentiable `n` times on a set `s` of `E` in the model with corners defined by `modelWithCornersSelf 𝕜 E` and `modelWithCornersSelf 𝕜 E'`, then `f` is continuously differentiable `n` times on `s` in the normed field `𝕜`.
More concisely: If a function $f:\ E \rightarrow E'$ is continuously differentiable $n$ times on a set $s$ in the model with corners of normed fields $\mathbb{K}, E,$ and $E'$, then $f$ is continuously differentiable $n$ times on $s$ in the normed field $\mathbb{K}$.
|
ContMDiffAt.contDiffAt
theorem ContMDiffAt.contDiffAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {x : E},
ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x → ContDiffAt 𝕜 n f x
This theorem, named `ContMDiffAt.contDiffAt`, is an alias for the forward direction of `contMDiffAt_iff_contDiffAt`. It states that for a given non-trivially normed field `𝕜`, normed add commutative groups `E` and `E'` that are also normed spaces over `𝕜`, a function `f` from `E` to `E'`, and a point `x` in `E`, if `f` is continuously differentiable at `x` under the model with corners `modelWithCornersSelf 𝕜 E` and `modelWithCornersSelf 𝕜 E'`, then `f` is continuously differentiable at `x` with respect to `𝕜`. Here, `n` is the order of differentiation, which can be a natural number or infinity (`ℕ∞`).
More concisely: If a function `f` from a normed space `E` to another normed space `E'` over a non-trivially normed field `𝕜` is continuously differentiable at a point `x` in `E` under the model with corners, then `f` is continuously differentiable at `x` with respect to `𝕜`.
|
Smooth.smul
theorem Smooth.smul :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
{M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V : Type u_18}
[inst_6 : NormedAddCommGroup V] [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
Smooth I (modelWithCornersSelf 𝕜 𝕜) f →
Smooth I (modelWithCornersSelf 𝕜 V) g → Smooth I (modelWithCornersSelf 𝕜 V) fun p => f p • g p
The theorem `Smooth.smul` states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `V`, and a topological space `H`, if we have a smooth function `f` from a topological manifold `M` with corners to `𝕜` and another smooth function `g` from `M` to `V`, then the function `p => f p • g p` which maps every point `p` of the manifold to the scalar multiplication of the function values `f(p)` and `g(p)` is also smooth. Here, smoothness is relative to the model with corners `I` for `M` and the standard model with corners for either `𝕜` or `V`.
More concisely: If `f` is a smooth function from a topological manifold `M` with corners to a non-trivially normed field, and `g` is another smooth function from `M` to a normed additive commutative group, then the function `p => f(p) • g(p)` is smooth.
|
ContMDiffWithinAt.contDiffWithinAt
theorem ContMDiffWithinAt.contDiffWithinAt :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {s : Set E} {x : E},
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x → ContDiffWithinAt 𝕜 n f s x
This theorem, also known as the forward direction of `contMDiffWithinAt_iff_contDiffWithinAt`, states that for any non-trivial normed field `𝕜`, any normed add commutative groups `E` and `E'` over `𝕜`, any function `f` from `E` to `E'`, any set `s` of elements of `E`, any element `x` of `E`, and any natural number or infinity `n`, if the function `f` is continuously differentiable at `x` within `s`, in the sense of the model with corners self on `E` and `E'`, then `f` is continuously differentiable at `x` within `s` in the sense of the standard definition of differential calculus. The model with corners self provides a convenient framework to study smooth manifolds with corners, introducing a structure of vector space on the space of differentiable functions.
More concisely: If a function is continuously differentiable at a point with respect to a set in the sense of the model with corners, then it is continuously differentiable at that point with respect to the set in the standard sense in Lean 4 for non-trivial normed fields and normed add commutative groups.
|
ContDiffOn.contMDiffOn
theorem ContDiffOn.contMDiffOn :
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {n : ℕ∞}
{f : E → E'} {s : Set E},
ContDiffOn 𝕜 n f s → ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s
This theorem is an alias for the reverse direction of `contMDiffOn_iff_contDiffOn`. It states that if a function `f` from a normed additive commutative group `E` to another such group `E'` is continuously differentiable over a certain set `s` of `E`, then it is also continuously differentiable in the sense of manifolds with corners over the same set `s`, when the model with corners is given by the identity (represented by `modelWithCornersSelf`) on both the domain and the target. Here, the field `𝕜` is a nontrivially normed field, `n` is the degree of differentiability, which can be an arbitrary natural number or infinity (`ℕ∞`), and `s` is a set of elements from `E`. The conditions `inst`, `inst_1`, `inst_2`, `inst_3` and `inst_4` are requirements for the field `𝕜` to be nontrivially normed and for `E` and `E'` to be normed additive commutative groups where `𝕜` is also a normed space.
More concisely: If a continuously differentiable function `f` from a normed additive commutative group `E` to another `E'`, with `𝕜` as the common nontrivially normed field, is defined on a set `s`, then `f` is also continuously differentiable as a function between manifolds with corners over `s` using the identity models on both `E` and `E'`.
|