arclength of a function

Stream: Is there code for X?

[Callum Cassidy-Nolan]

I'm trying to figure out if there is code to figure out the arclength of a continuous function, does it exist?

[Jireh Loreaux]

What context do you want exactly? Are you thinking of a function defined on a closed interval in ℝ taking values in a metric space (i.e., {X : Type*} [metric_space X] (a b : ℝ) (f : set.interval a b → X))?

[Jireh Loreaux]

And what definition of arc length do you want? The supremum of the sums between distances of images under the function (where the supremum ranges over all finite partitions of the interval)?

[Callum Cassidy-Nolan]

What you've described sounds good

[Callum Cassidy-Nolan]

This is like the level I'd be working with it with: image.png

[Jireh Loreaux]

This involves considerably more machinery, but I think the API is developed relatively well by this point. Here, you perhaps want to work with a function f : ℝ → ℝ × ℝ which is continuously differentiable (i.e., (h : cont_diff ℝ 1 f). And then your integrand is ∥deriv f∥. You could take this (the interval_integral of this norm) as a definition of arc length if you wanted (although it's not going to be well-behaved / defined in more general circumstances).

[Jireh Loreaux]

I'm not sure exactly what you want to do (and I'll be away for a while after this message).