# arclength as filtered limit

The length (http://planetmath.org/Rectifiable) of a rectifiable curve may be phrased as a filtered limit.
To do this, we will define a filter of partitions of an interval^{}
$[a,b]$. Let $\mathbf{P}$ be the set of all ordered tuplets of distinct
elements of $[a,b]$ whose entries are increasing:

$$ |

We shall refer to elements of $\mathbf{P}$ as partitions of the interval
$[a,b]$. We shall say that $({t}_{1},\mathrm{\dots},{t}_{n})$ is a refinement^{} of a
partition $({s}_{1},\mathrm{\dots},{s}_{m})$ if $\{{t}_{1},\mathrm{\dots},{t}_{n}\}\supset \{{s}_{1},\mathrm{\dots},{s}_{m}\}$. Let $\mathbf{F}\subset \mathcal{P}(\mathbf{P})$ be the
set of all subsets of $\mathbf{P}$ such that, if a certain partition
belongs to $\mathbf{F}$ then so do all refinements of that partition.

Let us see that $\mathbf{F}$ is a filter basis. Suppose that $A$ and $B$ are elements of $\mathbf{F}$. If a partition belongs to both $A$ and $B$ then every one of its refinements will also belong to both $A$ and $B$, hence $A\cap B\in \mathbf{F}$.

Next, note that, if a partition of $B$ is a refinement of a partition
of $A$ then, by the triangle inequality^{}, the length of $\mathrm{\Pi}(B)$ is
greater than the length of $\mathrm{\Pi}(A)$. By definition, for every
$\u03f5>0$, we can pick a partition $A$ such that the length of
$\mathrm{\Pi}(A)$ differs from the length of the curve by at most $\u03f5$.
Since the length of $\mathrm{\Pi}(B)$ for any partition $B$ refining $A$ lies
between the length of $\mathrm{\Pi}(A)$ and the length of the curve, we see
that the length of $\mathrm{\Pi}(B)$ will also differ by at most $\u03f5$, so
the length of the curve is the limit of the length of polygonal lines
according to the filter generated by $\mathbf{F}$.

Title | arclength as filtered limit |
---|---|

Canonical name | ArclengthAsFilteredLimit |

Date of creation | 2013-03-22 15:49:34 |

Last modified on | 2013-03-22 15:49:34 |

Owner | rspuzio (6075) |

Last modified by | rspuzio (6075) |

Numerical id | 13 |

Author | rspuzio (6075) |

Entry type | Result |

Classification | msc 51N05 |