Length of a curve

TheoremIntegrating the norm of a derivative within a closed interval#✓fully proved

Let \(E\) be a real normed space, let \(f : \mathbb{R} \to E\) be any function and let \(a \le b\) be real numbers. Then \(\int_a^b \lVert f'(t) \rVert \, dt = \int_a^b \lVert f'_{[a,b]}(t) \rVert \, dt\), where \(f'(t)\) is the derivative of \(f\) at \(t\) and \(f'_{[a,b]}(t)\) is its derivative at \(t\) within \([a, b]\), each taken to be \(0\) where it does not exist.

theorem _root_.intervalIntegral.integral_norm_deriv_eq_integral_norm_derivWithin_Icc
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (f : ℝ → E) {a b : ℝ} (hab : a ≤ b) :
    (∫ t in a..b, ‖deriv f t‖) = ∫ t in a..b, ‖derivWithin f (Icc a b) t‖

Used by 1

Used byLength of a \(C^1\) curve

TheoremLength of a \(C^1\) curve via its derivative within the interval#✓fully proved

Let \(E\) be a real Banach space, let \(a \le b\) be real numbers and let \(\gamma : \mathbb{R} \to E\) be continuously differentiable on \([a, b]\). Then the total variation of \(\gamma\) on \([a, b]\), a priori a value in \([0, \infty]\), equals the real number \(\int_a^b \lVert \gamma'_{[a,b]}(t) \rVert \, dt\), where \(\gamma'_{[a,b]}(t)\) is the derivative of \(\gamma\) at \(t\) within \([a, b]\).

theorem _root_.ContDiffOn.eVariationOn_Icc_eq_ofReal_integral_norm_derivWithin
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {γ : ℝ → E} {a b : ℝ} (hab : a ≤ b)
    (hγ : ContDiffOn ℝ 1 γ (Icc a b)) :
    eVariationOn γ (Icc a b) =
      ENNReal.ofReal (∫ t in a..b, ‖derivWithin γ (Icc a b) t‖)

Used by 1

Used byLength of a \(C^1\) curve

TheoremLength of a \(C^1\) curve#✓fully proved

Let \(E\) be a real Banach space, let \(a \le b\) be real numbers, and let \(\gamma : \mathbb{R} \to E\) be continuously differentiable on \([a, b]\). Then the total variation of \(\gamma\) on \([a, b]\) (its length, a priori a value in \([0, \infty]\)) equals \(\int_a^b \lVert \gamma'(t) \rVert \, dt\).

Proof: Extend the derivative of \(\gamma\) relative to \([a, b]\) by zero outside the interval and identify the vector measure of its primitive with the corresponding density vector measure. The variation of that measure is the integral of the norm, and the ordinary derivative agrees with the derivative relative to \([a, b]\) almost everywhere on the interval.

theorem curve_length_eq_integral_norm_deriv
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {γ : ℝ → E} {a b : ℝ} (hab : a ≤ b)
    (hγ : ContDiffOn ℝ 1 γ (Set.Icc a b)) :
    eVariationOn γ (Set.Icc a b) = ENNReal.ofReal (∫ t in a..b, ‖deriv γ t‖)

Sources

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6; stable ref https://en.wikipedia.org/wiki/Arc_length.

Uses 2 · Used by 1

Proof usesLength of a \(C^1\) curve via its derivative within the interval · Integrating the norm of a derivative within a closed interval

Used byContour length of a \(C^1\) curve

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.