Ambient velocity on a compact part of a smooth motion

Let a boundaryless manifold M move through a finite-dimensional boundaryless manifold N by smooth embeddings. On any compact subset A of M, the velocity extends to a smooth ambient time-dependent vector field with support in a fixed compact subset of N, provided that the motion of A is stationary outside a bounded time interval. The source itself need not be compact. In particular, A can be a closed disc in an open-disc source.

The time-preserving track is an injective immersion. Its restriction to a precompact open neighbourhood of the compact portion under consideration is a topological embedding: it is a restriction of a continuous injection from the compact closure into a Hausdorff space. Extend the track velocity using Topology.IsEmbedding.exists_contMDiffSection_extension and cut off in time. This is the velocity-extension step in the proof of isotopy extension; integration of the field is separate.

TauCeti.exists_ambientVelocityField allows arbitrary codimension and loses one derivative. It requires stationarity only on the compact subset whose velocity is extended.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §1, Theorems 1.3--1.4 and their proof.

theorem TauCeti.exists_ambientVelocityField {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n m : ℕ∞} [IsManifold I (↑n) M] {G : ℝ × M → N} (hG : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) J (↑n) G) (hslice : ∀ (t : ℝ), Manifold.IsSmoothEmbedding I J ↑n fun (x : M) => G (t, x)) {A : Set M} (hA : IsCompact A) {a b : ℝ} (ha : ∀ t ≤ a, ∀ x ∈ A, G (t, x) = G (a, x)) (hb : ∀ (t : ℝ), b ≤ t → ∀ x ∈ A, G (t, x) = G (b, x)) (hm : 1 ≤ m) (hmn : m + 1 ≤ n) : ∃ (X : ℝ → (y : N) → TangentSpace J y) (K : Set N), IsCompact K ∧ (∀ (t : ℝ), ∀ y ∉ K, X t y = 0) ∧ (ContMDiff ((modelWithCornersSelf ℝ ℝ).prod J) J.tangent ↑m fun (p : ℝ × N) => ⟨p.2, X p.1 p.2⟩) ∧ ∀ (t : ℝ), ∀ x ∈ A, HasMFDerivAt% (fun (s : ℝ) => G (s, x)) t (ContinuousLinearMap.smulRight 1 (X t (G (t, x))))

A compact part of a motion through smooth embeddings moves along a compactly supported smooth ambient vector field. The source need not be compact, and stationarity outside the time interval [a, b] is required only on A. The field is jointly C^m in time and space when the motion is C^n, with 1 ≤ m and m + 1 ≤ n.