C^n bundled maps

In this file we define the type ContMDiffMap of n times continuously differentiable bundled maps.

def ContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u_7) [TopologicalSpace M'] [ChartedSpace H' M'] (n : WithTop ℕ∞) : Type (max 0 u_6 u_7)

Bundled n times continuously differentiable maps, denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with the trivial model) in the Manifold namespace.

Equations

• ContMDiffMap I I' M M' n = { f : M → M' // ContMDiff I I' n f }

def Manifold.«termC^_⟮_,_;_,_⟯» : Lean.ParserDescr

Bundled n times continuously differentiable maps, denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with the trivial model) in the Manifold namespace.

Equations

• One or more equations did not get rendered due to their size.

def Manifold.«termC^_⟮_,_;_⟯» : Lean.ParserDescr

Bundled n times continuously differentiable maps, denoted as C^n(I, M; I', M') and C^n(I, M; k) (when the target is a normed space k with the trivial model) in the Manifold namespace.

Equations

• One or more equations did not get rendered due to their size.

instance ContMDiffMap.instFunLike {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} : FunLike (ContMDiffMap I I' M M' n) M M'

Equations

• ContMDiffMap.instFunLike = { coe := Subtype.val, coe_injective' := ⋯ }

theorem ContMDiffMap.contMDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (f : ContMDiffMap I I' M M' n) : ContMDiff I I' n ⇑f

@[simp]

theorem ContMDiffMap.coeFn_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (f : M → M') (hf : ContMDiff I I' n f) : ⇑⟨f, hf⟩ = f

theorem ContMDiffMap.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} ⦃f g : ContMDiffMap I I' M M' n⦄ (h : ⇑f = ⇑g) : f = g

theorem ContMDiffMap.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} {f g : ContMDiffMap I I' M M' n} (h : ∀ (x : M), f x = g x) : f = g

theorem ContMDiffMap.ext_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} {f g : ContMDiffMap I I' M M' n} : f = g ↔ ∀ (x : M), f x = g x

instance ContMDiffMap.instContinuousMapClass {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} : ContinuousMapClass (ContMDiffMap I I' M M' n) M M'

def ContMDiffMap.id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} : ContMDiffMap I I M M n

The identity as a C^n map.

Equations

• ContMDiffMap.id = ⟨id, ⋯⟩

def ContMDiffMap.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : WithTop ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) : ContMDiffMap I I'' M M'' n

The composition of C^n maps, as a C^n map.

Equations

• f.comp g = ⟨fun (a : M) => f (g a), ⋯⟩

@[simp]

theorem ContMDiffMap.comp_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type u_9} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [TopologicalSpace M''] [ChartedSpace H'' M''] {n : WithTop ℕ∞} (f : ContMDiffMap I' I'' M' M'' n) (g : ContMDiffMap I I' M M' n) (x : M) : (f.comp g) x = f (g x)

instance ContMDiffMap.instInhabited {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} [Inhabited M'] : Inhabited (ContMDiffMap I I' M M' n)

Equations

• ContMDiffMap.instInhabited = { default := ⟨fun (x : M) => default, ⋯⟩ }

def ContMDiffMap.const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} (y : M') : ContMDiffMap I I' M M' n

Constant map as a C^n map

Equations

• ContMDiffMap.const y = ⟨fun (x : M) => y, ⋯⟩

def ContMDiffMap.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} : ContMDiffMap (I.prod I') I (M × M') M n

The first projection of a product, as a C^n map.

Equations

• ContMDiffMap.fst = ⟨Prod.fst, ⋯⟩

def ContMDiffMap.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {n : WithTop ℕ∞} : ContMDiffMap (I.prod I') I' (M × M') M' n

The second projection of a product, as a C^n map.

Equations

• ContMDiffMap.snd = ⟨Prod.snd, ⋯⟩

def ContMDiffMap.prodMk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_4} [TopologicalSpace H] {H' : Type u_5} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {F : Type u_11} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_12} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} (f : ContMDiffMap J I N M n) (g : ContMDiffMap J I' N M' n) : ContMDiffMap J (I.prod I') N (M × M') n

Given two C^n maps f and g, this is the C^n map x ↦ (f x, g x).

Equations

• f.prodMk g = ⟨fun (x : N) => (f x, g x), ⋯⟩

instance ContinuousLinearMap.hasCoeToContMDiffMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (n : WithTop ℕ∞) : Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)

Equations

• ContinuousLinearMap.hasCoeToContMDiffMap n = { coe := fun (f : E →L[𝕜] E') => ⟨⇑f, ⋯⟩ }