Vector fields read in the charts of a manifold modelled on its own model space

Let M be a manifold modelled on a real normed space E with the trivial model 𝓘(ℝ, E). A vector field V on E pulls back by a chart e of the maximal atlas to the field VectorField.mpullback 𝓘(ℝ, E) 𝓘(ℝ, E) e V on the source of e. This file computes the chart derivative of the pullback and the derivative of a function along it, and shows that it is smooth when V is. The pullbacks of constant fields in the preferred chart give, near any regular point of a smooth function, a smooth field along which the function strictly decreases; finitely many of them, cut off by bump functions, give a global field of unit-speed decrease near any compact set of regular points.

Main declarations

• TauCeti.mfderiv_mpullback_apply, TauCeti.mvfderiv_mpullback_apply, TauCeti.contMDiffOn_mpullback: the pullback of a vector field by a chart.
• TauCeti.chartConstField: a constant field in the preferred chart at a point, on the manifold.
• TauCeti.mvfderiv_chartConstField_apply: the derivative of a function along a constant chart field, read in the chart.
• TauCeti.exists_mem_nhds_mvfderiv_chartConstField_lt_zero: near a regular point of a smooth function, some constant field in the preferred chart is a direction of strict decrease.
• TauCeti.exists_mem_nhds_contMDiffOn_mvfderiv_eq_neg_one: near a regular point of a smooth function, a rescaled constant chart field is a smooth direction of unit-speed decrease.
• TauCeti.exists_vectorField_mvfderiv_eq_neg_one: a smooth vector field, vanishing outside a compact set, with df(X) ≤ 0 everywhere and df(X) = -1 on a neighbourhood of a compact set of regular points.

theorem TauCeti.mfderiv_mpullback_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) 1 M) (V : (z : E) → TangentSpace (modelWithCornersSelf ℝ E) z) {y : M} (hy : y ∈ e.source) : (mfderiv% ↑e y) (VectorField.mpullback (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑e) V y) = V (↑e y)

The pullback de_y⁻¹ (V (e y)) of a vector field V on the model space by a chart e.

theorem TauCeti.mvfderiv_mpullback_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} {e : OpenPartialHomeomorph M E} {h : E → ℝ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) 1 M) (hfh : Set.EqOn f (h ∘ ↑e) e.source) (V : (z : E) → TangentSpace (modelWithCornersSelf ℝ E) z) {y : M} (hy : y ∈ e.source) : (d% f y) (VectorField.mpullback (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑e) V y) = (fderiv ℝ h (↑e y)) (V (↑e y))

The derivative of f along the pullback of a vector field V by a chart e, where f = h ∘ e on the source of e.

theorem TauCeti.contMDiffOn_mpullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} [FiniteDimensional ℝ E] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) (↑⊤) M) {V : (z : E) → TangentSpace (modelWithCornersSelf ℝ E) z} (hV : ContDiffOn ℝ (↑⊤) V e.target) : ContMDiffOn (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E).tangent (↑⊤) (fun (y : M) => ⟨y, VectorField.mpullback (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E) (↑e) V y⟩) e.source

The pullback of a smooth vector field on the model space by a chart of the maximal atlas is smooth on the source of the chart.

noncomputable def TauCeti.constVectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v z : E) : TangentSpace (modelWithCornersSelf ℝ E) z

The constant vector field with value v on the model space.

theorem TauCeti.constVectorField_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v z : E) : constVectorField v z = (NormedSpace.fromTangentSpace z).symm v

The constant vector field takes the value v at every point, under the canonical identification NormedSpace.fromTangentSpace of each tangent space of E with E.

theorem TauCeti.contMDiff_constVectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) {n : WithTop ℕ∞} : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E).tangent n fun (z : E) => ⟨z, constVectorField v z⟩

The constant vector field is smooth.

noncomputable def TauCeti.chartConstField (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] (p : M) (v : E) (y : M) : TangentSpace (modelWithCornersSelf ℝ E) y

The constant vector field with value v in the preferred chart at p, pulled back to the manifold.

theorem TauCeti.contMDiffOn_chartConstField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [FiniteDimensional ℝ E] (p : M) (v : E) : ContMDiffOn (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E).tangent (↑⊤) (fun (y : M) => ⟨y, chartConstField E p v y⟩) (chartAt E p).source

A constant field in a chart is smooth on the source of the chart.

theorem TauCeti.mvfderiv_chartConstField_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} [IsManifold (modelWithCornersSelf ℝ E) 1 M] {y₀ y : M} (v : E) (hy : y ∈ (chartAt E y₀).source) : (d% f y) (chartConstField E y₀ v y) = (fderiv ℝ (f ∘ ↑(chartAt E y₀).symm) (↑(chartAt E y₀) y)) v

On the source of the preferred chart at y₀, the derivative of f along a constant chart field with value v is the derivative of f ∘ (chartAt E y₀).symm in the direction v.

theorem TauCeti.exists_mem_nhds_mvfderiv_chartConstField_lt_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (hf : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) f) {y₀ : M} (hcrit : mfderiv% f y₀ ≠ 0) : ∃ (v : E), ∃ U ∈ nhds y₀, U ⊆ (chartAt E y₀).source ∧ ∀ y ∈ U, (d% f y) (chartConstField E y₀ v y) < 0

Near a regular point of f, some constant field in the preferred chart is a direction of strict decrease of f.

theorem TauCeti.exists_mem_nhds_contMDiffOn_mvfderiv_eq_neg_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} [FiniteDimensional ℝ E] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (hf : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) f) {y₀ : M} (hcrit : mfderiv% f y₀ ≠ 0) : ∃ U ∈ nhds y₀, ∃ (s : (y : M) → TangentSpace (modelWithCornersSelf ℝ E) y), ContMDiffOn (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E).tangent (↑⊤) (fun (y : M) => ⟨y, s y⟩) U ∧ ∀ y ∈ U, (d% f y) (s y) = -1

Near a regular point of a smooth function f, there is a smooth local vector field along which f decreases at unit speed, df(s) = -1.

theorem TauCeti.exists_vectorField_mvfderiv_eq_neg_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] {f : M → ℝ} [FiniteDimensional ℝ E] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [T2Space M] (hf : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) f) {K : Set M} (hK : IsCompact K) (hreg : ∀ x ∈ K, mfderiv% f x ≠ 0) : ∃ (X : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x), (ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E).tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) ∧ (∀ (x : M), (d% f x) (X x) ≤ 0) ∧ (∃ (U : Set M), IsOpen U ∧ K ⊆ U ∧ ∀ x ∈ U, (d% f x) (X x) = -1) ∧ ∃ (C : Set M), IsCompact C ∧ ∀ x ∉ C, X x = 0

A unit-speed descending field near a compact set of regular points. If a compact set K contains no critical point of the smooth function f, there is a smooth vector field X, vanishing outside a compact set, along which f never increases, df(X) ≤ 0, and with df(X) = -1 on an open neighbourhood of K.