Smooth maps from products

Mathlib equips a product of model vector spaces both with the product of their self-models and with the self-model of the product. This file provides the C^n bridge between those definitionally distinct presentations.

These bridges are useful when transporting C^n and C^n-on-a-set statements between product chart coordinates and the self-model of the product model space.

The file also records a tube lemma: a map from a product which is C^n at every point of a compact slice {x} × K is C^n on a product of open neighbourhoods of x and of K.

Main results

• contMDiff_prod_modelWithCornersSelf_iff: a map from a product of model vector spaces is C^n for the product of the self-models if and only if it is C^n for the self-model of the product.
• contMDiffOn_prod_modelWithCornersSelf_iff: the same bridge for C^n maps on a set.
• TauCeti.exists_isOpen_prod_contMDiffOn: the tube lemma for maps from a product which are C^n along a compact slice.

theorem contMDiff_prod_modelWithCornersSelf_iff {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E' : Type u_4} {H' : Type u_5} {M : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H' M] {n : WithTop ℕ∞} {f : E₁ × E₂ → M} : ContMDiff ((modelWithCornersSelf 𝕜 E₁).prod (modelWithCornersSelf 𝕜 E₂)) I' n f ↔ ContMDiff (modelWithCornersSelf 𝕜 (E₁ × E₂)) I' n f

A map from a product of model vector spaces is C^n for the product of the self-models if and only if it is C^n for the self-model of the product.

theorem contMDiffOn_prod_modelWithCornersSelf_iff {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E' : Type u_4} {H' : Type u_5} {M : Type u_6} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H' M] {n : WithTop ℕ∞} {f : E₁ × E₂ → M} {s : Set (E₁ × E₂)} : ContMDiffOn ((modelWithCornersSelf 𝕜 E₁).prod (modelWithCornersSelf 𝕜 E₂)) I' n f s ↔ ContMDiffOn (modelWithCornersSelf 𝕜 (E₁ × E₂)) I' n f s

A map from a product of model vector spaces is C^n on a set for the product of the self-models if and only if it is C^n on that set for the self-model of the product.

theorem TauCeti.exists_isOpen_prod_contMDiffOn {𝕜 : Type u_1} {E' : Type u_4} {H' : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [TopologicalSpace Y] [ChartedSpace H' (X × Y)] {F : Type u_9} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_10} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] [IsManifold I' n (X × Y)] [IsManifold J n N] {f : X × Y → N} {x : X} {K : Set Y} (hK : IsCompact K) (hn : n ≠ ↑⊤) (hf : ∀ y ∈ K, ContMDiffAt I' J n f (x, y)) : ∃ (U : Set X) (V : Set Y), IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ K ⊆ V ∧ ContMDiffOn I' J n f (U ×ˢ V)

The tube lemma for C^n maps from a product. If f : X × Y → N is C^n at every point of {x} × K with K compact and n ≠ ∞, then f is C^n on U ×ˢ V for some open neighbourhoods U of x and V of K.