LeanPool.DirectedTopologyLean4.SplitPath.SplitPath

def SplitPath.FirstPart {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (T : ↑unitInterval) : Path x₀ (γ T)

The part of a path on the interval [0, T]

Equations

• SplitPath.FirstPart γ T = { toFun := fun (t : ↑unitInterval) => γ ⟨↑T * ↑t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

def SplitPath.SecondPart {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (T : ↑unitInterval) : Path (γ T) x₁

The part of a path on the interval [T, 1]

Equations

• SplitPath.SecondPart γ T = { toFun := fun (t : ↑unitInterval) => γ ⟨↑(unitInterval.symm T) * ↑t + ↑T, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

noncomputable def SplitPath.transReparam (T t : ↑unitInterval) : ℝ

The map needed to reparametrize the concatenation of the first and second part of a path back into the original pat

Equations

• SplitPath.transReparam T t = if ↑t ≤ ↑T then ↑t / (2 * ↑T) else (1 + ↑t - 2 * ↑T) / (2 * (1 - ↑T))

theorem SplitPath.continuous_trans_reparam {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : Continuous (transReparam T)

theorem SplitPath.trans_reparam_mem_I (t : ↑unitInterval) {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : transReparam T t ∈ unitInterval

theorem SplitPath.trans_reparam_zero (T : ↑unitInterval) : transReparam T 0 = 0

theorem SplitPath.trans_reparam_one {T : ↑unitInterval} (hT₁ : T < 1) : transReparam T 1 = 1

theorem SplitPath.monotone_trans_reparam {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : Monotone (transReparam T)

theorem SplitPath.first_trans_second_reparam_eq_self_aux {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) (t : ↑unitInterval) {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : γ t = (((FirstPart γ T).trans (SecondPart γ T)).reparam (fun (t : ↑unitInterval) => ⟨transReparam T t, ⋯⟩) ⋯ ⋯ ⋯) t

theorem SplitPath.first_trans_second_reparam_eq_self {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Path x₀ x₁) {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : γ = ((FirstPart γ T).trans (SecondPart γ T)).reparam (fun (t : ↑unitInterval) => ⟨transReparam T t, ⋯⟩) ⋯ ⋯ ⋯