The almost-everywhere chain rule for absolutely continuous curves

Composing an absolutely continuous curve in a finite-dimensional real normed space with a monotone or antitone absolutely continuous change of parameter satisfies the chain rule almost everywhere. The derivative formula includes constant pieces and unbounded speeds.

theorem AbsolutelyContinuousOnInterval.ae_hasDerivAt_comp_of_monotoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) (hmap : Set.MapsTo θ (Set.Icc a b) (Set.uIcc c d)) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → HasDerivAt (γ ∘ θ) (deriv θ t • deriv γ (θ t)) t

The chain rule almost everywhere for an absolutely continuous curve under a monotone absolutely continuous change of parameter.

theorem AbsolutelyContinuousOnInterval.ae_deriv_comp_of_monotoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hmono : MonotoneOn θ (Set.Icc a b)) (hmap : Set.MapsTo θ (Set.Icc a b) (Set.uIcc c d)) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → deriv (γ ∘ θ) t = deriv θ t • deriv γ (θ t)

The canonical derivative satisfies the chain rule almost everywhere under a monotone absolutely continuous change of parameter.

theorem AbsolutelyContinuousOnInterval.ae_hasDerivAt_comp_of_antitoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (hmap : Set.MapsTo θ (Set.Icc a b) (Set.uIcc c d)) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → HasDerivAt (γ ∘ θ) (deriv θ t • deriv γ (θ t)) t

The chain rule almost everywhere for an absolutely continuous curve under an antitone absolutely continuous change of parameter.

theorem AbsolutelyContinuousOnInterval.ae_deriv_comp_of_antitoneOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {θ : ℝ → ℝ} {a b c d : ℝ} (hγ : AbsolutelyContinuousOnInterval γ c d) (hθ : AbsolutelyContinuousOnInterval θ a b) (hab : a ≤ b) (hanti : AntitoneOn θ (Set.Icc a b)) (hmap : Set.MapsTo θ (Set.Icc a b) (Set.uIcc c d)) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → deriv (γ ∘ θ) t = deriv θ t • deriv γ (θ t)

The canonical derivative satisfies the chain rule almost everywhere under an antitone absolutely continuous change of parameter.