How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Complex path length is invariant under monotone surjective reparametrization
Statement
Let and . Suppose is continuous and is continuous, surjective, and either nondecreasing or nonincreasing in the sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences. Then
The equality includes finite and infinite lengths, constant pauses, reversal, and singleton intervals. A nondecreasing map preserves parameter order; a nonincreasing map reverses it. When , is constant and there is no nontrivial orientation to distinguish.
Facts & Assumptions
Given: The intervals, continuous path, and continuous surjective monotone map in the statement.
Polygonal length and rectifiability of complex paths: A complex path must be continuous from the usual real metric to , and its length is the extended-real supremum of its partition sums, with singleton length zero.
The complex coordinate isometry transports topology and affine segments and Complex path length equals coordinate length and piecewise speed integral: is an isometry and the length of every continuous complex path equals that of its coordinate path, including singleton intervals.
Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal: A continuous surjective nondecreasing or nonincreasing reparametrization preserves Euclidean polygonal length, including pauses, reversal, and singleton intervals.
Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of , with the dictionary to monotone sequences: Nondecreasing maps preserve order and nonincreasing maps reverse order.
Continuity of a map between metric spaces, at a point and globally, in the - form, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane, The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded, and Intervals of : the nine order-convex forms, nondegeneracy, and length: Continuity is the metric - condition on the indicated interval subspaces; the real metric is and the complex metric is .
Proof
The composite is continuous. Indeed, fix and . By continuity of at choose such that and imply . By continuity of at choose such that and imply . The implication in [F5] then proves continuity of the composite at .
If , surjectivity forces , so both lengths are zero by [F1]. If while , then and are constant paths and both lengths are zero by [F1]. Thus the equality covers all singleton cases.
Put . By the isometry in [F2], is continuous and . The Euclidean reparametrization theorem [F3] gives .
Apply the complex-to-coordinate length equality [F2] to and, using step 1.1, to . Together with step 2.1 this yields .
By [F4], the nondecreasing case preserves order and the nonincreasing case reverses it. If , a nondecreasing surjection must attain at and at ; a nonincreasing surjection must attain at and at . If , the map is constant and there is no nontrivial orientation.
Depends on
- Polygonal length and rectifiability of complex paths
- The complex coordinate isometry transports topology and affine segments
- Complex path length equals coordinate length and piecewise speed integral
- Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $\mathbb{R}$, with the dictionary to monotone sequences
- The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane
- Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$-$\delta$ form
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- The absolute value makes $\mathbb{R}$ a metric space: $d(x,y) = |x-y|$ is a metric, its open balls are the intervals $(x-r, x+r)$, and it is unbounded
Used by
Dependency tree · two levels
50 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- E. Stein and R. Shakarchi, Complex Analysis, Princeton Lectures in Analysis II, Chapter 1, Section 3 (standard reference, not scraped)
- U. Lang, Differential Geometry I, Section 1.1 (standard reference, not scraped)