mathlib3 documentation

geometry.manifold.mfderiv

The derivative of functions between smooth manifolds #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let M and M' be two smooth manifolds with corners over a field 𝕜 (with respective models with corners I on (E, H) and I' on (E', H')), and let f : M → M'. We define the derivative of the function at a point, within a set or along the whole space, mimicking the API for (Fréchet) derivatives. It is denoted by mfderiv I I' f x, where "m" stands for "manifold" and "f" for "Fréchet" (as in the usual derivative fderiv 𝕜 f x).

Main definitions #

Let f be a map between smooth manifolds. The following definitions follow the fderiv API.

We also establish results on the differential of the identity, constant functions, charts, extended charts. For functions between vector spaces, we show that the usual notions and the manifold notions coincide.

Implementation notes #

The tangent bundle is constructed using the machinery of topological fiber bundles, for which one can define bundled morphisms and construct canonically maps from the total space of one bundle to the total space of another one. One could use this mechanism to construct directly the derivative of a smooth map. However, we want to define the derivative of any map (and let it be zero if the map is not differentiable) to avoid proof arguments everywhere. This means we have to go back to the details of the definition of the total space of a fiber bundle constructed from core, to cook up a suitable definition of the derivative. It is the following: at each point, we have a preferred chart (used to identify the fiber above the point with the model vector space in fiber bundles). Then one should read the function using these preferred charts at x and f x, and take the derivative of f in these charts.

Due to the fact that we are working in a model with corners, with an additional embedding I of the model space H in the model vector space E, the charts taking values in E are not the original charts of the manifold, but those ones composed with I, called extended charts. We define written_in_ext_chart I I' x f for the function f written in the preferred extended charts. Then the manifold derivative of f, at x, is just the usual derivative of written_in_ext_chart I I' x f, at the point (ext_chart_at I x) x.

There is a subtelty with respect to continuity: if the function is not continuous, then the image of a small open set around x will not be contained in the source of the preferred chart around f x, which means that when reading f in the chart one is losing some information. To avoid this, we include continuity in the definition of differentiablity (which is reasonable since with any definition, differentiability implies continuity).

Warning: the derivative (even within a subset) is a linear map on the whole tangent space. Suppose that one is given a smooth submanifold N, and a function which is smooth on N (i.e., its restriction to the subtype N is smooth). Then, in the whole manifold M, the property mdifferentiable_on I I' f N holds. However, mfderiv_within I I' f N is not uniquely defined (what values would one choose for vectors that are transverse to N?), which can create issues down the road. The problem here is that knowing the value of f along N does not determine the differential of f in all directions. This is in contrast to the case where N would be an open subset, or a submanifold with boundary of maximal dimension, where this issue does not appear. The predicate unique_mdiff_on I N indicates that the derivative along N is unique if it exists, and is an assumption in most statements requiring a form of uniqueness.

On a vector space, the manifold derivative and the usual derivative are equal. This means in particular that they live on the same space, i.e., the tangent space is defeq to the original vector space. To get this property is a motivation for our definition of the tangent space as a single copy of the vector space, instead of more usual definitions such as the space of derivations, or the space of equivalence classes of smooth curves in the manifold.

Tags #

Derivative, manifold

Derivative of maps between manifolds #

The derivative of a smooth map f between smooth manifold M and M' at x is a bounded linear map from the tangent space to M at x, to the tangent space to M' at f x. Since we defined the tangent space using one specific chart, the formula for the derivative is written in terms of this specific chart.

We use the names mdifferentiable and mfderiv, where the prefix letter m means "manifold".

def differentiable_within_at_prop {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') (f : H H') (s : set H) (x : H) :
Prop

Property in the model space of a model with corners of being differentiable within at set at a point, when read in the model vector space. This property will be lifted to manifolds to define differentiable functions between manifolds.

Equations

Being differentiable in the model space is a local property, invariant under smooth maps. Therefore, it will lift nicely to manifolds.

def unique_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] (s : set M) (x : M) :
Prop

Predicate ensuring that, at a point and within a set, a function can have at most one derivative. This is expressed using the preferred chart at the considered point.

Equations
def unique_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] (s : set M) :
Prop

Predicate ensuring that, at all points of a set, a function can have at most one derivative.

Equations
def mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') (s : set M) (x : M) :
Prop

mdifferentiable_within_at I I' f s x indicates that the function f between manifolds has a derivative at the point x within the set s. This is a generalization of differentiable_within_at to manifolds.

We require continuity in the definition, as otherwise points close to x in s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence written_in_ext_chart_at I I' x f could be differentiable, while this would not mean anything relevant.

Equations
theorem mdifferentiable_within_at_iff_lift_prop_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') (s : set M) (x : M) :
def mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') (x : M) :
Prop

mdifferentiable_at I I' f x indicates that the function f between manifolds has a derivative at the point x. This is a generalization of differentiable_at to manifolds.

We require continuity in the definition, as otherwise points close to x could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence written_in_ext_chart_at I I' x f could be differentiable, while this would not mean anything relevant.

Equations
theorem mdifferentiable_at_iff_lift_prop_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') (x : M) :
def mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') (s : set M) :
Prop

mdifferentiable_on I I' f s indicates that the function f between manifolds has a derivative within s at all points of s. This is a generalization of differentiable_on to manifolds.

Equations
def mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : M M') :
Prop

mdifferentiable I I' f indicates that the function f between manifolds has a derivative everywhere. This is a generalization of differentiable to manifolds.

Equations
def local_homeomorph.mdifferentiable {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] (f : local_homeomorph M M') :
Prop

Prop registering if a local homeomorphism is a local diffeomorphism on its source

Equations
def has_mfderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') (s : set M) (x : M) (f' : tangent_space I x →L[𝕜] tangent_space I' (f x)) :
Prop

has_mfderiv_within_at I I' f s x f' indicates that the function f between manifolds has, at the point x and within the set s, the derivative f'. Here, f' is a continuous linear map from the tangent space at x to the tangent space at f x.

This is a generalization of has_fderiv_within_at to manifolds (as indicated by the prefix m). The order of arguments is changed as the type of the derivative f' depends on the choice of x.

We require continuity in the definition, as otherwise points close to x in s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence written_in_ext_chart_at I I' x f could be differentiable, while this would not mean anything relevant.

Equations
def has_mfderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') (x : M) (f' : tangent_space I x →L[𝕜] tangent_space I' (f x)) :
Prop

has_mfderiv_at I I' f x f' indicates that the function f between manifolds has, at the point x, the derivative f'. Here, f' is a continuous linear map from the tangent space at x to the tangent space at f x.

We require continuity in the definition, as otherwise points close to x s could be sent by f outside of the chart domain around f x. Then the chart could do anything to the image points, and in particular by coincidence written_in_ext_chart_at I I' x f could be differentiable, while this would not mean anything relevant.

Equations
noncomputable def mfderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') (s : set M) (x : M) :

Let f be a function between two smooth manifolds. Then mfderiv_within I I' f s x is the derivative of f at x within s, as a continuous linear map from the tangent space at x to the tangent space at f x.

Equations
noncomputable def mfderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') (x : M) :

Let f be a function between two smooth manifolds. Then mfderiv I I' f x is the derivative of f at x, as a continuous linear map from the tangent space at x to the tangent space at f x.

Equations
noncomputable def tangent_map_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') (s : set M) :

The derivative within a set, as a map between the tangent bundles

Equations
noncomputable def tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] (f : M M') :

The derivative, as a map between the tangent bundles

Equations

Unique differentiability sets in manifolds #

theorem unique_mdiff_within_at.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {s t : set M} (h : unique_mdiff_within_at I s x) (st : s t) :
theorem unique_mdiff_within_at.inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {s t : set M} (hs : unique_mdiff_within_at I s x) (ht : t nhds_within x s) :
theorem unique_mdiff_within_at.inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {s t : set M} (hs : unique_mdiff_within_at I s x) (ht : t nhds x) :
theorem is_open.unique_mdiff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {x : M} {s : set M} (xs : x s) (hs : is_open s) :
theorem unique_mdiff_on.inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s t : set M} (hs : unique_mdiff_on I s) (ht : is_open t) :
theorem is_open.unique_mdiff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {s : set M} (hs : is_open s) :
theorem unique_mdiff_within_at.eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' f₁' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (U : unique_mdiff_within_at I s x) (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') :
f' = f₁'

unique_mdiff_within_at achieves its goal: it implies the uniqueness of the derivative.

theorem unique_mdiff_on.eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' f₁' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (U : unique_mdiff_on I s) (hx : x s) (h : has_mfderiv_within_at I I' f s x f') (h₁ : has_mfderiv_within_at I I' f s x f₁') :
f' = f₁'

General lemmas on derivatives of functions between manifolds #

We mimick the API for functions between vector spaces

theorem mdifferentiable_within_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} {x : M} :
theorem mdifferentiable_within_at_iff_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {x' : M} {y : M'} (hx : x' (charted_space.chart_at H x).to_local_equiv.source) (hy : f x' (charted_space.chart_at H' y).to_local_equiv.source) :

One can reformulate differentiability within a set at a point as continuity within this set at this point, and differentiability in any chart containing that point.

theorem mfderiv_within_zero_of_not_mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : ¬mdifferentiable_within_at I I' f s x) :
mfderiv_within I I' f s x = 0
theorem mfderiv_zero_of_not_mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : ¬mdifferentiable_at I I' f x) :
mfderiv I I' f x = 0
theorem has_mfderiv_within_at.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f t x f') (hst : s t) :
has_mfderiv_within_at I I' f s x f'
theorem has_mfderiv_at.has_mfderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_at I I' f x f') :
has_mfderiv_within_at I I' f s x f'
theorem has_mfderiv_within_at.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') :
theorem has_mfderiv_at.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_at I I' f x f') :
@[simp]
theorem has_mfderiv_within_at_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} :
theorem has_mfderiv_at_unique {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f₀' f₁' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h₀ : has_mfderiv_at I I' f x f₀') (h₁ : has_mfderiv_at I I' f x f₁') :
f₀' = f₁'
theorem has_mfderiv_within_at_inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : t nhds_within x s) :
has_mfderiv_within_at I I' f (s t) x f' has_mfderiv_within_at I I' f s x f'
theorem has_mfderiv_within_at_inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : t nhds x) :
has_mfderiv_within_at I I' f (s t) x f' has_mfderiv_within_at I I' f s x f'
theorem has_mfderiv_within_at.union {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (hs : has_mfderiv_within_at I I' f s x f') (ht : has_mfderiv_within_at I I' f t x f') :
has_mfderiv_within_at I I' f (s t) x f'
theorem has_mfderiv_within_at.nhds_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') (ht : s nhds_within x t) :
has_mfderiv_within_at I I' f t x f'
theorem has_mfderiv_within_at.has_mfderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') (hs : s nhds x) :
has_mfderiv_at I I' f x f'
theorem mdifferentiable_within_at.has_mfderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) :
has_mfderiv_within_at I I' f s x (mfderiv_within I I' f s x)
theorem mdifferentiable_within_at.mfderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) :
theorem mdifferentiable_at.has_mfderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_at I I' f x) :
has_mfderiv_at I I' f x (mfderiv I I' f x)
theorem mdifferentiable_at.mfderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_at I I' f x) :
theorem has_mfderiv_at.mfderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_at I I' f x f') :
mfderiv I I' f x = f'
theorem has_mfderiv_within_at.mfderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') (hxs : unique_mdiff_within_at I s x) :
mfderiv_within I I' f s x = f'
theorem mdifferentiable.mfderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_at I I' f x) (hxs : unique_mdiff_within_at I s x) :
mfderiv_within I I' f s x = mfderiv I I' f x
theorem mfderiv_within_subset {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (st : s t) (hs : unique_mdiff_within_at I s x) (h : mdifferentiable_within_at I I' f t x) :
mfderiv_within I I' f s x = mfderiv_within I I' f t x
theorem mdifferentiable_within_at.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} (hst : s t) (h : mdifferentiable_within_at I I' f t x) :
theorem mdifferentiable_within_at_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} :
theorem mdifferentiable_within_at_inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} (ht : t nhds x) :
theorem mdifferentiable_within_at_inter' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} (ht : t nhds_within x s) :
theorem mdifferentiable_at.mdifferentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} (h : mdifferentiable_at I I' f x) :
theorem mdifferentiable_within_at.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} (h : mdifferentiable_within_at I I' f s x) (hs : s nhds x) :
theorem mdifferentiable_on.mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s t : set M} (h : mdifferentiable_on I I' f t) (st : s t) :
theorem mdifferentiable_on_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} :
theorem mdifferentiable.mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} (h : mdifferentiable I I' f) :
theorem mdifferentiable_on_of_locally_mdifferentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} (h : (x : M), x s ( (u : set M), is_open u x u mdifferentiable_on I I' f (s u))) :
@[simp]
theorem mfderiv_within_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] :
theorem mfderiv_within_inter {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (ht : t nhds x) :
mfderiv_within I I' f (s t) x = mfderiv_within I I' f s x
theorem mdifferentiable_at_iff_of_mem_source {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {x' : M} {y : M'} (hx : x' (charted_space.chart_at H x).to_local_equiv.source) (hy : f x' (charted_space.chart_at H' y).to_local_equiv.source) :

Deriving continuity from differentiability on manifolds #

theorem has_mfderiv_within_at.continuous_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') :
theorem has_mfderiv_at.continuous_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_at I I' f x f') :
theorem mdifferentiable_within_at.continuous_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} {s : set M} (h : mdifferentiable_within_at I I' f s x) :
theorem mdifferentiable_at.continuous_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} (h : mdifferentiable_at I I' f x) :
theorem mdifferentiable_on.continuous_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} (h : mdifferentiable_on I I' f s) :
theorem mdifferentiable.continuous {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} (h : mdifferentiable I I' f) :
theorem tangent_map_within_subset {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {p : tangent_bundle I M} (st : s t) (hs : unique_mdiff_within_at I s p.proj) (h : mdifferentiable_within_at I I' f t p.proj) :
theorem tangent_map_within_univ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] :
theorem tangent_map_within_eq_tangent_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {p : tangent_bundle I M} (hs : unique_mdiff_within_at I s p.proj) (h : mdifferentiable_at I I' f p.proj) :
tangent_map_within I I' f s p = tangent_map I I' f p
@[simp]
theorem tangent_map_within_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {p : tangent_bundle I M} :
(tangent_map_within I I' f s p).proj = f p.proj
@[simp]
theorem tangent_map_proj {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {p : tangent_bundle I M} :
(tangent_map I I' f p).proj = f p.proj
theorem mdifferentiable_within_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {x : M} {s : set M} {f : M M'} {g : M M''} (hf : mdifferentiable_within_at I I' f s x) (hg : mdifferentiable_within_at I I'' g s x) :
mdifferentiable_within_at I (I'.prod I'') (λ (x : M), (f x, g x)) s x
theorem mdifferentiable_at.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {x : M} {f : M M'} {g : M M''} (hf : mdifferentiable_at I I' f x) (hg : mdifferentiable_at I I'' g x) :
mdifferentiable_at I (I'.prod I'') (λ (x : M), (f x, g x)) x
theorem mdifferentiable_on.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {s : set M} {f : M M'} {g : M M''} (hf : mdifferentiable_on I I' f s) (hg : mdifferentiable_on I I'' g s) :
mdifferentiable_on I (I'.prod I'') (λ (x : M), (f x, g x)) s
theorem mdifferentiable.prod_mk {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {g : M M''} (hf : mdifferentiable I I' f) (hg : mdifferentiable I I'' g) :
mdifferentiable I (I'.prod I'') (λ (x : M), (f x, g x))
theorem mdifferentiable_within_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {x : M} {s : set M} {f : M E'} {g : M E''} (hf : mdifferentiable_within_at I (model_with_corners_self 𝕜 E') f s x) (hg : mdifferentiable_within_at I (model_with_corners_self 𝕜 E'') g s x) :
mdifferentiable_within_at I (model_with_corners_self 𝕜 (E' × E'')) (λ (x : M), (f x, g x)) s x
theorem mdifferentiable_at.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {x : M} {f : M E'} {g : M E''} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f x) (hg : mdifferentiable_at I (model_with_corners_self 𝕜 E'') g x) :
mdifferentiable_at I (model_with_corners_self 𝕜 (E' × E'')) (λ (x : M), (f x, g x)) x
theorem mdifferentiable_on.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {s : set M} {f : M E'} {g : M E''} (hf : mdifferentiable_on I (model_with_corners_self 𝕜 E') f s) (hg : mdifferentiable_on I (model_with_corners_self 𝕜 E'') g s) :
mdifferentiable_on I (model_with_corners_self 𝕜 (E' × E'')) (λ (x : M), (f x, g x)) s
theorem mdifferentiable.prod_mk_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {f : M E'} {g : M E''} (hf : mdifferentiable I (model_with_corners_self 𝕜 E') f) (hg : mdifferentiable I (model_with_corners_self 𝕜 E'') g) :
mdifferentiable I (model_with_corners_self 𝕜 (E' × E'')) (λ (x : M), (f x, g x))

Congruence lemmas for derivatives on manifolds #

theorem has_mfderiv_within_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
has_mfderiv_within_at I I' f₁ s x f'
theorem has_mfderiv_within_at.congr_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_within_at I I' f s x f') (ht : (x : M), x t f₁ x = f x) (hx : f₁ x = f x) (h₁ : t s) :
has_mfderiv_within_at I I' f₁ t x f'
theorem has_mfderiv_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} (h : has_mfderiv_at I I' f x f') (h₁ : f₁ =ᶠ[nhds x] f) :
has_mfderiv_at I I' f₁ x f'
theorem mdifferentiable_within_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
theorem filter.eventually_eq.mdifferentiable_within_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
theorem mdifferentiable_within_at.congr_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) (ht : (x : M), x t f₁ x = f x) (hx : f₁ x = f x) (h₁ : t s) :
theorem mdifferentiable_within_at.congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) (ht : (x : M), x s f₁ x = f x) (hx : f₁ x = f x) :
theorem mdifferentiable_on.congr_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_on I I' f s) (h' : (x : M), x t f₁ x = f x) (h₁ : t s) :
mdifferentiable_on I I' f₁ t
theorem mdifferentiable_at.congr_of_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_at I I' f x) (hL : f₁ =ᶠ[nhds x] f) :
mdifferentiable_at I I' f₁ x
theorem mdifferentiable_within_at.mfderiv_within_congr_mono {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s t : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : mdifferentiable_within_at I I' f s x) (hs : (x : M), x t f₁ x = f x) (hx : f₁ x = f x) (hxt : unique_mdiff_within_at I t x) (h₁ : t s) :
mfderiv_within I I' f₁ t x = mfderiv_within I I' f s x
theorem filter.eventually_eq.mfderiv_within_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (hs : unique_mdiff_within_at I s x) (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
mfderiv_within I I' f₁ s x = mfderiv_within I I' f s x
theorem mfderiv_within_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (hs : unique_mdiff_within_at I s x) (hL : (x : M), x s f₁ x = f x) (hx : f₁ x = f x) :
mfderiv_within I I' f₁ s x = mfderiv_within I I' f s x
theorem tangent_map_within_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {s : set M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (h : (x : M), x s f x = f₁ x) (p : tangent_bundle I M) (hp : p.proj s) (hs : unique_mdiff_within_at I s p.proj) :
tangent_map_within I I' f s p = tangent_map_within I I' f₁ s p
theorem filter.eventually_eq.mfderiv_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f f₁ : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] (hL : f₁ =ᶠ[nhds x] f) :
mfderiv I I' f₁ x = mfderiv I I' f x
theorem mfderiv_congr_point {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {x' : M} (h : x = x') :
mfderiv I I' f x = mfderiv I I' f x'

A congruence lemma for mfderiv, (ab)using the fact that tangent_space I' (f x) is definitionally equal to E'.

theorem mfderiv_congr {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {f : M M'} {x : M} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] {f' : M M'} (h : f = f') :
mfderiv I I' f x = mfderiv I I' f' x

A congruence lemma for mfderiv, (ab)using the fact that tangent_space I' (f x) is definitionally equal to E'.

Composition lemmas #

theorem written_in_ext_chart_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {x : M} {s : set M} {g : M' M''} (h : continuous_within_at f s x) :
theorem has_mfderiv_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {s : set M} {g : M' M''} {u : set M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} {g' : tangent_space I' (f x) →L[𝕜] tangent_space I'' (g (f x))} (hg : has_mfderiv_within_at I' I'' g u (f x) g') (hf : has_mfderiv_within_at I I' f s x f') (hst : s f ⁻¹' u) :
has_mfderiv_within_at I I'' (g f) s x (g'.comp f')
theorem has_mfderiv_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} {g' : tangent_space I' (f x) →L[𝕜] tangent_space I'' (g (f x))} (hg : has_mfderiv_at I' I'' g (f x) g') (hf : has_mfderiv_at I I' f x f') :
has_mfderiv_at I I'' (g f) x (g'.comp f')

The chain rule.

theorem has_mfderiv_at.comp_has_mfderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {s : set M} {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] {f' : tangent_space I x →L[𝕜] tangent_space I' (f x)} {g' : tangent_space I' (f x) →L[𝕜] tangent_space I'' (g (f x))} (hg : has_mfderiv_at I' I'' g (f x) g') (hf : has_mfderiv_within_at I I' f s x f') :
has_mfderiv_within_at I I'' (g f) s x (g'.comp f')
theorem mdifferentiable_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {s : set M} {g : M' M''} {u : set M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable_within_at I' I'' g u (f x)) (hf : mdifferentiable_within_at I I' f s x) (h : s f ⁻¹' u) :
theorem mdifferentiable_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable_at I' I'' g (f x)) (hf : mdifferentiable_at I I' f x) :
mdifferentiable_at I I'' (g f) x
theorem mfderiv_within_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {s : set M} {g : M' M''} {u : set M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable_within_at I' I'' g u (f x)) (hf : mdifferentiable_within_at I I' f s x) (h : s f ⁻¹' u) (hxs : unique_mdiff_within_at I s x) :
mfderiv_within I I'' (g f) s x = (mfderiv_within I' I'' g u (f x)).comp (mfderiv_within I I' f s x)
theorem mfderiv_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} (x : M) {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable_at I' I'' g (f x)) (hf : mdifferentiable_at I I' f x) :
mfderiv I I'' (g f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
theorem mfderiv_comp_of_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] {x : M} {y : M'} (hg : mdifferentiable_at I' I'' g y) (hf : mdifferentiable_at I I' f x) (hy : f x = y) :
mfderiv I I'' (g f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
theorem mdifferentiable_on.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {s : set M} {g : M' M''} {u : set M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable_on I' I'' g u) (hf : mdifferentiable_on I I' f s) (st : s f ⁻¹' u) :
mdifferentiable_on I I'' (g f) s
theorem mdifferentiable.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable I' I'' g) (hf : mdifferentiable I I' f) :
mdifferentiable I I'' (g f)
theorem tangent_map_within_comp_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {s : set M} {g : M' M''} {u : set M'} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (p : tangent_bundle I M) (hg : mdifferentiable_within_at I' I'' g u (f p.proj)) (hf : mdifferentiable_within_at I I' f s p.proj) (h : s f ⁻¹' u) (hps : unique_mdiff_within_at I s p.proj) :
tangent_map_within I I'' (g f) s p = tangent_map_within I' I'' g u (tangent_map_within I I' f s p)
theorem tangent_map_comp_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (p : tangent_bundle I M) (hg : mdifferentiable_at I' I'' g (f p.proj)) (hf : mdifferentiable_at I I' f p.proj) :
tangent_map I I'' (g f) p = tangent_map I' I'' g (tangent_map I I' f p)
theorem tangent_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {f : M M'} {g : M' M''} [Is : smooth_manifold_with_corners I M] [I's : smooth_manifold_with_corners I' M'] [I''s : smooth_manifold_with_corners I'' M''] (hg : mdifferentiable I' I'' g) (hf : mdifferentiable I I' f) :
tangent_map I I'' (g f) = tangent_map I' I'' g tangent_map I I' f

Relations between vector space derivative and manifold derivative #

The manifold derivative mfderiv, when considered on the model vector space with its trivial manifold structure, coincides with the usual Frechet derivative fderiv. In this section, we prove this and related statements.

@[simp]
theorem written_in_ext_chart_model_space {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f : E E'} {x : E} :

Alias of the forward direction of has_mfderiv_at_iff_has_fderiv_at.

Alias of the reverse direction of has_mfderiv_at_iff_has_fderiv_at.

For maps between vector spaces, mdifferentiable_within_at and fdifferentiable_within_at coincide

For maps between vector spaces, mdifferentiable_at and differentiable_at coincide

Alias of the forward direction of mdifferentiable_at_iff_differentiable_at.

Alias of the reverse direction of mdifferentiable_at_iff_differentiable_at.

For maps between vector spaces, mdifferentiable_on and differentiable_on coincide

Alias of the forward direction of mdifferentiable_on_iff_differentiable_on.

Alias of the reverse direction of mdifferentiable_on_iff_differentiable_on.

For maps between vector spaces, mdifferentiable and differentiable coincide

Alias of the forward direction of mdifferentiable_iff_differentiable.

Alias of the reverse direction of mdifferentiable_iff_differentiable.

@[simp]
theorem mfderiv_within_eq_fderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f : E E'} {s : set E} {x : E} :

For maps between vector spaces, mfderiv_within and fderiv_within coincide

@[simp]
theorem mfderiv_eq_fderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f : E E'} {x : E} :

For maps between vector spaces, mfderiv and fderiv coincide

Differentiability of specific functions #

@[protected]
theorem continuous_linear_map.has_mfderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : E →L[𝕜] E') {s : set E} {x : E} :
@[protected]
theorem continuous_linear_map.has_mfderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : E →L[𝕜] E') {x : E} :
@[protected]
@[protected]
@[protected]
@[protected]
theorem continuous_linear_map.mfderiv_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : E →L[𝕜] E') {x : E} :
@[protected]
@[protected]
theorem continuous_linear_equiv.has_mfderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : E ≃L[𝕜] E') {x : E} :
@[protected]
@[protected]
@[protected]
theorem continuous_linear_equiv.mfderiv_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : E ≃L[𝕜] E') {x : E} :

Identity #

@[simp]
theorem mfderiv_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {x : M} :
theorem mfderiv_within_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {x : M} (hxs : unique_mdiff_within_at I s x) :
@[simp]
theorem tangent_map_within_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {p : tangent_bundle I M} (hs : unique_mdiff_within_at I s p.proj) :

Constants #

theorem has_mfderiv_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (c : M') (x : M) :
has_mfderiv_at I I' (λ (y : M), c) x 0
theorem has_mfderiv_within_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (c : M') (s : set M) (x : M) :
has_mfderiv_within_at I I' (λ (y : M), c) s x 0
theorem mdifferentiable_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M} {c : M'} :
mdifferentiable_at I I' (λ (y : M), c) x
theorem mdifferentiable_within_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set M} {x : M} {c : M'} :
mdifferentiable_within_at I I' (λ (y : M), c) s x
theorem mdifferentiable_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {c : M'} :
mdifferentiable I I' (λ (y : M), c)
theorem mdifferentiable_on_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set M} {c : M'} :
mdifferentiable_on I I' (λ (y : M), c) s
@[simp]
theorem mfderiv_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M} {c : M'} :
mfderiv I I' (λ (y : M), c) x = 0
theorem mfderiv_within_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set M} {x : M} {c : M'} (hxs : unique_mdiff_within_at I s x) :
mfderiv_within I I' (λ (y : M), c) s x = 0

Operations on the product of two manifolds

theorem has_mfderiv_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (x : M × M') :
theorem has_mfderiv_within_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (s : set (M × M')) (x : M × M') :
theorem mdifferentiable_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M × M'} :
theorem mdifferentiable_within_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {x : M × M'} :
theorem mdifferentiable_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] :
theorem mdifferentiable_on_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} :
@[simp]
theorem mfderiv_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M × M'} :
theorem mfderiv_within_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {x : M × M'} (hxs : unique_mdiff_within_at (I.prod I') s x) :
@[simp]
theorem tangent_map_prod_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {p : tangent_bundle (I.prod I') (M × M')} :
tangent_map (I.prod I') I prod.fst p = {proj := p.proj.fst, snd := p.snd.fst}
theorem tangent_map_within_prod_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {p : tangent_bundle (I.prod I') (M × M')} (hs : unique_mdiff_within_at (I.prod I') s p.proj) :
theorem has_mfderiv_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (x : M × M') :
theorem has_mfderiv_within_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (s : set (M × M')) (x : M × M') :
theorem mdifferentiable_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M × M'} :
theorem mdifferentiable_within_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {x : M × M'} :
theorem mdifferentiable_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] :
theorem mdifferentiable_on_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} :
@[simp]
theorem mfderiv_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x : M × M'} :
theorem mfderiv_within_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {x : M × M'} (hxs : unique_mdiff_within_at (I.prod I') s x) :
@[simp]
theorem tangent_map_prod_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {p : tangent_bundle (I.prod I') (M × M')} :
tangent_map (I.prod I') I' prod.snd p = {proj := p.proj.snd, snd := p.snd.snd}
theorem tangent_map_within_prod_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {s : set (M × M')} {p : tangent_bundle (I.prod I') (M × M')} (hs : unique_mdiff_within_at (I.prod I') s p.proj) :
tangent_map_within (I.prod I') I' prod.snd s p = {proj := p.proj.snd, snd := p.snd.snd}
theorem mdifferentiable_at.mfderiv_prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] [smooth_manifold_with_corners I'' M''] {f : M M'} {g : M M''} {x : M} (hf : mdifferentiable_at I I' f x) (hg : mdifferentiable_at I I'' g x) :
mfderiv I (I'.prod I'') (λ (x : M), (f x, g x)) x = (mfderiv I I' f x).prod (mfderiv I I'' g x)
theorem mfderiv_prod_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x₀ : M} {y₀ : M'} :
mfderiv I (I.prod I') (λ (x : M), (x, y₀)) x₀ = continuous_linear_map.inl 𝕜 (tangent_space I x₀) (tangent_space I' y₀)
theorem mfderiv_prod_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {x₀ : M} {y₀ : M'} :
mfderiv I' (I.prod I') (λ (y : M'), (x₀, y)) y₀ = continuous_linear_map.inr 𝕜 (tangent_space I x₀) (tangent_space I' y₀)
theorem mfderiv_prod_eq_add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] (I : model_with_corners 𝕜 E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] (I' : model_with_corners 𝕜 E' H') {M' : Type u_7} [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] (I'' : model_with_corners 𝕜 E'' H'') {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] [smooth_manifold_with_corners I'' M''] {f : M × M' M''} {p : M × M'} (hf : mdifferentiable_at (I.prod I') I'' f p) :
mfderiv (I.prod I') I'' f p = show E × E' →L[𝕜] E'', from mfderiv (I.prod I') I'' (λ (z : M × M'), f (z.fst, p.snd)) p + mfderiv (I.prod I') I'' (λ (z : M × M'), f (p.fst, z.snd)) p

The total derivative of a function in two variables is the sum of the partial derivatives. Note that to state this (without casts) we need to be able to see through the definition of tangent_space.

Arithmetic #

Note that in the in has_mfderiv_at lemmas there is an abuse of the defeq between E' and tangent_space 𝓘(𝕜, E') (f z) (similarly for g',F',p',q'). In general this defeq is not canonical, but in this case (the tangent space of a vector space) it is canonical.

theorem has_mfderiv_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} {f' g' : tangent_space I z →L[𝕜] E'} (hf : has_mfderiv_at I (model_with_corners_self 𝕜 E') f z f') (hg : has_mfderiv_at I (model_with_corners_self 𝕜 E') g z g') :
has_mfderiv_at I (model_with_corners_self 𝕜 E') (f + g) z (f' + g')
theorem mdifferentiable_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (hg : mdifferentiable_at I (model_with_corners_self 𝕜 E') g z) :
theorem mdifferentiable.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f g : M E'} (hf : mdifferentiable I (model_with_corners_self 𝕜 E') f) (hg : mdifferentiable I (model_with_corners_self 𝕜 E') g) :
theorem mfderiv_add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (hg : mdifferentiable_at I (model_with_corners_self 𝕜 E') g z) :
theorem has_mfderiv_at.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} {f' : tangent_space I z →L[𝕜] E'} (hf : has_mfderiv_at I (model_with_corners_self 𝕜 E') f z f') (s : 𝕜) :
has_mfderiv_at I (model_with_corners_self 𝕜 E') (s f) z (s f')
theorem mdifferentiable_at.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (s : 𝕜) :
theorem mdifferentiable.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f : M E'} (s : 𝕜) (hf : mdifferentiable I (model_with_corners_self 𝕜 E') f) :
theorem const_smul_mfderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (s : 𝕜) :
theorem has_mfderiv_at.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} {f' : tangent_space I z →L[𝕜] E'} (hf : has_mfderiv_at I (model_with_corners_self 𝕜 E') f z f') :
theorem has_mfderiv_at_neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} {f' : tangent_space I z →L[𝕜] E'} :
theorem mdifferentiable_at.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) :
theorem mdifferentiable.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f : M E'} (hf : mdifferentiable I (model_with_corners_self 𝕜 E') f) :
theorem mfderiv_neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] (f : M E') (x : M) :
theorem has_mfderiv_at.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} {f' g' : tangent_space I z →L[𝕜] E'} (hf : has_mfderiv_at I (model_with_corners_self 𝕜 E') f z f') (hg : has_mfderiv_at I (model_with_corners_self 𝕜 E') g z g') :
has_mfderiv_at I (model_with_corners_self 𝕜 E') (f - g) z (f' - g')
theorem mdifferentiable_at.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (hg : mdifferentiable_at I (model_with_corners_self 𝕜 E') g z) :
theorem mdifferentiable.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {f g : M E'} (hf : mdifferentiable I (model_with_corners_self 𝕜 E') f) (hg : mdifferentiable I (model_with_corners_self 𝕜 E') g) :
theorem mfderiv_sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {z : M} {f g : M E'} (hf : mdifferentiable_at I (model_with_corners_self 𝕜 E') f z) (hg : mdifferentiable_at I (model_with_corners_self 𝕜 E') g z) :
theorem has_mfderiv_within_at.mul' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {z : M} {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} {p' q' : tangent_space I z →L[𝕜] F'} (hp : has_mfderiv_within_at I (model_with_corners_self 𝕜 F') p s z p') (hq : has_mfderiv_within_at I (model_with_corners_self 𝕜 F') q s z q') :
has_mfderiv_within_at I (model_with_corners_self 𝕜 F') (p * q) s z (p z q' + p'.smul_right (q z))
theorem has_mfderiv_at.mul' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {z : M} {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} {p' q' : tangent_space I z →L[𝕜] F'} (hp : has_mfderiv_at I (model_with_corners_self 𝕜 F') p z p') (hq : has_mfderiv_at I (model_with_corners_self 𝕜 F') q z q') :
has_mfderiv_at I (model_with_corners_self 𝕜 F') (p * q) z (p z q' + p'.smul_right (q z))
theorem mdifferentiable_within_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {z : M} {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} (hp : mdifferentiable_within_at I (model_with_corners_self 𝕜 F') p s z) (hq : mdifferentiable_within_at I (model_with_corners_self 𝕜 F') q s z) :
theorem mdifferentiable_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {z : M} {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} (hp : mdifferentiable_at I (model_with_corners_self 𝕜 F') p z) (hq : mdifferentiable_at I (model_with_corners_self 𝕜 F') q z) :
theorem mdifferentiable_on.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} (hp : mdifferentiable_on I (model_with_corners_self 𝕜 F') p s) (hq : mdifferentiable_on I (model_with_corners_self 𝕜 F') q s) :
theorem mdifferentiable.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {F' : Type u_11} [normed_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} (hp : mdifferentiable I (model_with_corners_self 𝕜 F') p) (hq : mdifferentiable I (model_with_corners_self 𝕜 F') q) :
theorem has_mfderiv_within_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {s : set M} {z : M} {F' : Type u_11} [normed_comm_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} {p' q' : tangent_space I z →L[𝕜] F'} (hp : has_mfderiv_within_at I (model_with_corners_self 𝕜 F') p s z p') (hq : has_mfderiv_within_at I (model_with_corners_self 𝕜 F') q s z q') :
has_mfderiv_within_at I (model_with_corners_self 𝕜 F') (p * q) s z (p z q' + q z p')
theorem has_mfderiv_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {z : M} {F' : Type u_11} [normed_comm_ring F'] [normed_algebra 𝕜 F'] {p q : M F'} {p' q' : tangent_space I z →L[𝕜] F'} (hp : has_mfderiv_at I (model_with_corners_self 𝕜 F') p z p') (hq : has_mfderiv_at I (model_with_corners_self 𝕜 F') q z q') :
has_mfderiv_at I (model_with_corners_self 𝕜 F') (p * q) z (p z q' + q z p')

Model with corners #

@[protected]
@[protected]
@[protected]

The derivative of the chart at a base point is the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

The derivative of the inverse of the chart at a base point is the inverse of the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

Differentiable local homeomorphisms #

@[protected]
theorem local_homeomorph.mdifferentiable.mdifferentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {e : local_homeomorph M M'} (he : local_homeomorph.mdifferentiable I I' e) {x : M} (hx : x e.to_local_equiv.source) :
theorem local_homeomorph.mdifferentiable.mdifferentiable_at_symm {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {e : local_homeomorph M M'} (he : local_homeomorph.mdifferentiable I I' e) {x : M'} (hx : x e.to_local_equiv.target) :
@[protected]
noncomputable def local_homeomorph.mdifferentiable.mfderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {e : local_homeomorph M M'} (he : local_homeomorph.mdifferentiable I I' e) [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] {x : M} (hx : x e.to_local_equiv.source) :

The derivative of a differentiable local homeomorphism, as a continuous linear equivalence between the tangent spaces at x and e x.

Equations
theorem local_homeomorph.mdifferentiable.trans {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {E'' : Type u_8} [normed_add_comm_group E''] [normed_space 𝕜 E''] {H'' : Type u_9} [topological_space H''] {I'' : model_with_corners 𝕜 E'' H''} {M'' : Type u_10} [topological_space M''] [charted_space H'' M''] {e : local_homeomorph M M'} (he : local_homeomorph.mdifferentiable I I' e) {e' : local_homeomorph M' M''} [smooth_manifold_with_corners I M] [smooth_manifold_with_corners I' M'] [smooth_manifold_with_corners I'' M''] (he' : local_homeomorph.mdifferentiable I' I'' e') :

Differentiability of ext_chart_at #

Unique derivative sets in manifolds #

If a set has the unique differential property, then its image under a local diffeomorphism also has the unique differential property.

If a set in a manifold has the unique derivative property, then its pullback by any extended chart, in the vector space, also has the unique derivative property.

theorem unique_mdiff_on.unique_diff_on_inter_preimage {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {H : Type u_3} [topological_space H] {I : model_with_corners 𝕜 E H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {E' : Type u_5} [normed_add_comm_group E'] [normed_space 𝕜 E'] {H' : Type u_6} [topological_space H'] {I' : model_with_corners 𝕜 E' H'} {M' : Type u_7} [topological_space M'] [charted_space H' M'] {s : set M} (hs : unique_mdiff_on I s) (x : M) (y : M') {f : M M'} (hf : continuous_on f s) :

When considering functions between manifolds, this statement shows up often. It entails the unique differential of the pullback in extended charts of the set where the function can be read in the charts.

In a smooth fiber bundle, the preimage under the projection of a set with unique differential in the basis also has unique differential.