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.continuous_map_class
- cont_mdiff_map.inhabited
- continuous_linear_map.has_coe_to_cont_mdiff_map
- diffeomorph.cont_mdiff_map.has_coe
- 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
@[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
@[protected, instance]
def
cont_mdiff_map.continuous_map_class
{π : 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 : ββ} :
continuous_map_class (cont_mdiff_map I I' M M' n) M M'
Equations
- cont_mdiff_map.continuous_map_class = {coe := Ξ» (f : cont_mdiff_map I I' M M' n), βf, coe_injective' := _, map_continuous := _}
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 := _}}