Smooth concatenation of isotopies

Concatenate two smooth isotopies by traversing the first in the first quarter of the interval and the second in the last quarter. Both motions are stationary on an open neighbourhood of the joining time, so their concatenation is jointly smooth. This works at finite regularity and at C^∞; no analytic concatenation is asserted.

The smoothing uses Mathlib's Real.smoothTransition, following the stationary-time reparametrization in Hirsch, Differential Topology, Chapter 8, §8.1.

noncomputable def TauCeti.SmoothIsotopy.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f₀ f₁ f₂ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (G : SmoothIsotopy f₁ f₂) (hn : n ≤ ↑⊤) : SmoothIsotopy f₀ f₂

Concatenate smooth isotopies, making the motion stationary around the join. Finite differentiability and C^∞ are allowed.

@[simp]

theorem TauCeti.SmoothIsotopy.trans_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f₀ f₁ f₂ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (G : SmoothIsotopy f₁ f₂) (hn : n ≤ ↑⊤) (p : ↑unitInterval × M) : (F.trans G hn) p = if ↑p.1 ≤ 1 / 2 then F (⟨(4 * ↑p.1).smoothTransition, ⋯⟩, p.2) else G (⟨(4 * ↑p.1 - 3).smoothTransition, ⋯⟩, p.2)

The concatenation traverses the first isotopy at smoothed speed in the first half, and the second at smoothed speed in the second half.

theorem TauCeti.SmoothIsotopy.trans_apply_of_mem_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f₀ f₁ f₂ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (G : SmoothIsotopy f₁ f₂) (hn : n ≤ ↑⊤) {t : ↑unitInterval} (ht : ↑t ∈ Set.Icc (1 / 4) (3 / 4)) (x : M) : (F.trans G hn) (t, x) = f₁ x

The concatenation is stationary at the common endpoint throughout the middle half.

theorem TauCeti.SmoothIsotopy.trans_apply_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f₀ f₁ f₂ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (G : SmoothIsotopy f₁ f₂) (hn : n ≤ ↑⊤) {x : M} {s : Set N} (hF : ∀ (t : ↑unitInterval), F (t, x) ∈ s) (hG : ∀ (t : ↑unitInterval), G (t, x) ∈ s) (t : ↑unitInterval) : (F.trans G hn) (t, x) ∈ s

At each source point, the concatenation only takes values that one of the two isotopies takes at that point.

theorem TauCeti.SmoothIsotopic.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H : Type u_3} [TopologicalSpace H] {H' : Type u_4} [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f₀ f₁ f₂ : ContMDiffMap I J M N n} (h₀₁ : SmoothIsotopic f₀ f₁) (h₁₂ : SmoothIsotopic f₁ f₂) (hn : n ≤ ↑⊤) : SmoothIsotopic f₀ f₂

Smooth isotopy is transitive at finite regularity and at C^∞.