Nonzero derivatives of nonconstant absolutely continuous curves #
Every nonconstant absolutely continuous curve in a finite-dimensional real normed space admits an
interior parameter with nonzero derivative: if the derivative vanished at every interior point of
differentiability, almost-everywhere differentiability
(BoundedVariationOn.ae_differentiableAt_of_mem_uIcc) and
AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero would force the curve to be constant.
theorem
AbsolutelyContinuousOnInterval.exists_mem_Ioo_hasDerivAt_ne_zero
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{γ : ℝ → F}
{a b : ℝ}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hnonconst : ∃ s ∈ Set.Icc a b, ∃ t ∈ Set.Icc a b, γ s ≠ γ t)
:
∃ t₀ ∈ Set.Ioo a b, ∃ (v : F), v ≠ 0 ∧ HasDerivAt γ v t₀
Every nonconstant absolutely continuous curve on [a, b] has an interior point with nonzero
derivative.