theorem Reparametrization.smooth_increasing_has_smooth_inverse (I_tilde : Set ℝ) (hI : Convex ℝ I_tilde) (ψ : ℝ → ℝ) (hψ_smooth : ContDiffOn ℝ ⊤ ψ I_tilde) (hψ_pos : ∀ t ∈ I_tilde, 0 < derivWithin ψ I_tilde t) : Convex ℝ (ψ '' I_tilde) ∧ Set.InjOn ψ I_tilde ∧ ∃ (φ : ℝ → ℝ), ContDiffOn ℝ ⊤ φ (ψ '' I_tilde) ∧ (∀ t ∈ I_tilde, φ (ψ t) = t) ∧ (∀ s ∈ ψ '' I_tilde, ψ (φ s) = s) ∧ ∀ t ∈ I_tilde, derivWithin φ (ψ '' I_tilde) (ψ t) = (derivWithin ψ I_tilde t)⁻¹

theorem Reparametrization.smooth_increasing_has_smooth_inverse_global (ψ : ℝ → ℝ) (hψ : ContDiff ℝ ⊤ ψ) (hψ' : ∀ (t : ℝ), 0 < deriv ψ t) : Function.Injective ψ ∧ ∃ (φ : ℝ → ℝ), Function.LeftInverse φ ψ ∧ Function.RightInverse φ ψ ∧ ContDiff ℝ ⊤ φ ∧ ∀ (t : ℝ), deriv φ (ψ t) = (deriv ψ t)⁻¹

theorem Reparametrization.reparametrize_to_graph (d : ℝ → Fin 2 → ℝ) (hd : ContDiff ℝ ⊤ d) (hd1 : ∀ (t : ℝ), 0 < deriv (fun (s : ℝ) => d s 0) t) : ∃ (f : ℝ → ℝ) (φ : ℝ → ℝ), ContDiff ℝ ⊤ f ∧ ContDiff ℝ ⊤ φ ∧ ∀ (t : ℝ), d (φ t) = ![t, f t]

theorem Reparametrization.exists_smooth_arclength (d : ℝ → Fin 2 → ℝ) (hd : ContDiff ℝ ⊤ d) (hreg : ∀ (t : ℝ), deriv d t ≠ 0) : ∃ (ψ : ℝ → ℝ), ContDiff ℝ ⊤ ψ ∧ ∀ (t : ℝ), deriv ψ t = ‖deriv d t‖

theorem Reparametrization.exists_unit_speed_reparametrization (d : ℝ → Fin 2 → ℝ) (hd : ContDiff ℝ ⊤ d) (hreg : ∀ (t : ℝ), deriv d t ≠ 0) : ∃ (φ : ℝ → ℝ), ContDiff ℝ ⊤ φ ∧ (∀ (t : ℝ), deriv φ t > 0) ∧ ∀ (t : ℝ), ‖deriv (d ∘ φ) t‖ = 1