Smooth bundled map #
In this file we define the type cont_mdiff_map of n times continuously differentiable
bundled maps.
structure
cont_mdiff_map
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
(I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H')
(M : Type u_6)
[topological_space M]
[charted_space H M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M']
(n : ℕ∞) :
Type (max u_6 u_7)
- to_fun : M → M'
- cont_mdiff_to_fun : cont_mdiff I I' n self.to_fun
Bundled n times continuously differentiable maps.
Instances for cont_mdiff_map
- cont_mdiff_map.has_sizeof_inst
- cont_mdiff_map.has_coe_to_fun
- cont_mdiff_map.continuous_map.has_coe
- cont_mdiff_map.inhabited
- continuous_linear_map.has_coe_to_cont_mdiff_map
- smooth_map.has_mul
- smooth_map.has_add
- smooth_map.has_one
- smooth_map.has_zero
- smooth_map.semigroup
- smooth_map.add_semigroup
- smooth_map.monoid
- smooth_map.add_monoid
- smooth_map.comm_monoid
- smooth_map.add_comm_monoid
- smooth_map.group
- smooth_map.add_group
- smooth_map.comm_group
- smooth_map.add_comm_group
- smooth_map.semiring
- smooth_map.ring
- smooth_map.comm_ring
- smooth_map.has_smul
- smooth_map.module
- smooth_map.algebra
- smooth_map.has_smul'
- smooth_map.module'
- smooth_functions_algebra
- smooth_functions_tower
- pointed_smooth_map.cont_mdiff_map.algebra
- pointed_smooth_map.cont_mdiff_map.is_scalar_tower
- diffeomorph.cont_mdiff_map.has_coe
@[reducible]
def
smooth_map
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
(I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H')
(M : Type u_6)
[topological_space M]
[charted_space H M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M'] :
Type (max u_6 u_7)
Bundled smooth maps.
Equations
- smooth_map I I' M M' = cont_mdiff_map I I' M M' ⊤
@[protected, instance]
def
cont_mdiff_map.has_coe_to_fun
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
has_coe_to_fun (cont_mdiff_map I I' M M' n) (λ (_x : cont_mdiff_map I I' M M' n), M → M')
Equations
@[protected, instance]
def
cont_mdiff_map.continuous_map.has_coe
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
has_coe (cont_mdiff_map I I' M M' n) C(M, M')
Equations
- cont_mdiff_map.continuous_map.has_coe = {coe := λ (f : cont_mdiff_map I I' M M' n), {to_fun := ⇑f, continuous_to_fun := _}}
@[simp]
theorem
cont_mdiff_map.coe_fn_mk
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : M → M')
(hf : cont_mdiff I I' n f) :
⇑{to_fun := f, cont_mdiff_to_fun := hf} = f
@[protected]
theorem
cont_mdiff_map.cont_mdiff
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : cont_mdiff_map I I' M M' n) :
cont_mdiff I I' n ⇑f
@[protected]
theorem
cont_mdiff_map.smooth
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤) :
@[protected]
theorem
cont_mdiff_map.mdifferentiable'
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : cont_mdiff_map I I' M M' n)
(hn : 1 ≤ n) :
mdifferentiable I I' ⇑f
@[protected]
theorem
cont_mdiff_map.mdifferentiable
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤) :
mdifferentiable I I' ⇑f
@[protected]
theorem
cont_mdiff_map.mdifferentiable_at
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤)
{x : M} :
mdifferentiable_at I I' ⇑f x
theorem
cont_mdiff_map.coe_inj
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
⦃f g : cont_mdiff_map I I' M M' n⦄
(h : ⇑f = ⇑g) :
f = g
@[ext]
theorem
cont_mdiff_map.ext
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
{f g : cont_mdiff_map I I' M M' n}
(h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
def
cont_mdiff_map.id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{n : ℕ∞} :
cont_mdiff_map I I M M n
The identity as a smooth map.
Equations
- cont_mdiff_map.id = {to_fun := id M, cont_mdiff_to_fun := _}
def
cont_mdiff_map.comp
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{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'']
{n : ℕ∞}
(f : cont_mdiff_map I' I'' M' M'' n)
(g : cont_mdiff_map I I' M M' n) :
cont_mdiff_map I I'' M M'' n
The composition of smooth maps, as a smooth map.
@[simp]
theorem
cont_mdiff_map.comp_apply
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{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'']
{n : ℕ∞}
(f : cont_mdiff_map I' I'' M' M'' n)
(g : cont_mdiff_map I I' M M' n)
(x : M) :
@[protected, instance]
def
cont_mdiff_map.inhabited
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
[inhabited M'] :
inhabited (cont_mdiff_map I I' M M' n)
Equations
- cont_mdiff_map.inhabited = {default := {to_fun := λ (_x : M), inhabited.default, cont_mdiff_to_fun := _}}
def
cont_mdiff_map.const
{𝕜 : 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']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(y : M') :
cont_mdiff_map I I' M M' n
Constant map as a smooth map
Equations
- cont_mdiff_map.const y = {to_fun := λ (x : M), y, cont_mdiff_to_fun := _}
@[protected, instance]
def
continuous_linear_map.has_coe_to_cont_mdiff_map
{𝕜 : 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']
(n : ℕ∞) :
has_coe (E →L[𝕜] E') (cont_mdiff_map (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n)
Equations
- continuous_linear_map.has_coe_to_cont_mdiff_map n = {coe := λ (f : E →L[𝕜] E'), {to_fun := f.to_linear_map.to_fun, cont_mdiff_to_fun := _}}