Derivatives of extended concatenated paths

Away from the joining parameter 1/2, the derivative is twice the derivative of the corresponding component at its rescaled parameter. No differentiability assumption is needed: these formulas use Mathlib's total derivative, which is zero at nondifferentiability points. They follow from the local concatenation identities and affine derivative composition.

theorem Path.deriv_extend_trans_of_lt_half {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {p q r : E} (γ : Path p q) (δ : Path q r) {t : ℝ} (ht : t < 1 / 2) : deriv (⇑(γ.trans δ).extend) t = 2 • deriv (⇑γ.extend) (2 * t)

Below the joining parameter, the derivative comes from the first path at twice the speed.

theorem Path.deriv_extend_trans_of_half_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {p q r : E} (γ : Path p q) (δ : Path q r) {t : ℝ} (ht : 1 / 2 < t) : deriv (⇑(γ.trans δ).extend) t = 2 • deriv (⇑δ.extend) (2 * t - 1)

Above the joining parameter, the derivative comes from the second path at twice the speed.