Truncating and dropping the start of Moore paths

For a Moore path γ and a time s, the truncation γ.truncate s is the initial piece of γ up to time s: it has length min s γ.length and is stopped from time s on. The drop γ.drop s is the remaining piece, t ↦ γ (s + t), of length γ.length - s. The two pieces concatenate back to γ (MoorePath.truncate_trans_drop), with no reparametrization, and both depend continuously on the path and the time (Continuous.moorePath_truncate, Continuous.moorePath_drop).

These are the pieces from which the lifting function of a Moore-path replacement and the shrinking homotopies of the fibre are built.

Main definitions

• TauCeti.MoorePath.truncate γ s: the initial piece of γ up to time s.
• TauCeti.MoorePath.drop γ s: the piece of γ from time s on.

Main results

• TauCeti.MoorePath.truncate_trans_drop: γ.truncate s followed by γ.drop s is γ.
• TauCeti.MoorePath.truncate_trans_of_le, TauCeti.MoorePath.truncate_trans_length_add: the truncations of a concatenation.

Truncation

def TauCeti.MoorePath.truncate {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : MoorePath X

The truncation of a Moore path at time s: the path t ↦ γ (min t s), of length min s γ.length.

@[simp]

theorem TauCeti.MoorePath.truncate_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s t : NNReal) : (γ.truncate s).toContinuousMap t = γ.toContinuousMap (min t s)

@[simp]

theorem TauCeti.MoorePath.length_truncate {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.truncate s).length = min s γ.length

@[simp]

theorem TauCeti.MoorePath.source_truncate {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.truncate s).source = γ.source

@[simp]

theorem TauCeti.MoorePath.target_truncate {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.truncate s).target = γ.toContinuousMap s

@[simp]

theorem TauCeti.MoorePath.truncate_zero {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.truncate 0 = refl γ.source

theorem TauCeti.MoorePath.truncate_of_length_le {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) {s : NNReal} (hs : γ.length ≤ s) : γ.truncate s = γ

Truncating a Moore path at a time after its length changes nothing.

@[simp]

theorem TauCeti.MoorePath.truncate_length {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.truncate γ.length = γ

@[simp]

theorem TauCeti.MoorePath.map_truncate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) (s : NNReal) : map f (γ.truncate s) = (map f γ).truncate s

theorem Continuous.moorePath_truncate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y : Y) => (f y).truncate (g y)

Truncations form a continuous family in the path and the time.

theorem Continuous.moorePath_retrace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y : Y) => ((f y).truncate (g y)).trans ((f y).truncate (g y)).symm ⋯

A truncated path followed by its reversal varies continuously with the path and time, without requiring fixed endpoints.

theorem TauCeti.MoorePath.truncate_trans_of_le {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) {s : NNReal} (hs : s ≤ γ.length) : (γ.trans δ h).truncate s = γ.truncate s

Truncating a concatenation before the end of its first piece truncates the first piece.

theorem TauCeti.MoorePath.truncate_trans_length_add {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) (u : NNReal) : (γ.trans δ h).truncate (γ.length + u) = γ.trans (δ.truncate u) ⋯

Truncating a concatenation after the end of its first piece concatenates the first piece with a truncation of the second.

Dropping an initial piece

def TauCeti.MoorePath.drop {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : MoorePath X

The Moore path γ from time s on: the path t ↦ γ (s + t), of length γ.length - s.

@[simp]

theorem TauCeti.MoorePath.drop_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s t : NNReal) : (γ.drop s).toContinuousMap t = γ.toContinuousMap (s + t)

@[simp]

theorem TauCeti.MoorePath.length_drop {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.drop s).length = γ.length - s

@[simp]

theorem TauCeti.MoorePath.source_drop {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.drop s).source = γ.toContinuousMap s

@[simp]

theorem TauCeti.MoorePath.target_drop {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.drop s).target = γ.target

@[simp]

theorem TauCeti.MoorePath.drop_zero {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.drop 0 = γ

theorem TauCeti.MoorePath.drop_of_length_le {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) {s : NNReal} (hs : γ.length ≤ s) : γ.drop s = refl γ.target

Dropping a Moore path from a time after its length leaves the constant path at its target.

@[simp]

theorem TauCeti.MoorePath.drop_length {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.drop γ.length = refl γ.target

@[simp]

theorem TauCeti.MoorePath.map_drop {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) (s : NNReal) : map f (γ.drop s) = (map f γ).drop s

theorem Continuous.moorePath_drop {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y : Y) => (f y).drop (g y)

The pieces of a Moore path form a continuous family in the path and the time.

theorem TauCeti.MoorePath.truncate_trans_drop {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : NNReal) : (γ.truncate s).trans (γ.drop s) ⋯ = γ

A Moore path is the concatenation of its truncation at s with its piece from s on.