Alphabeta MathHow 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.
Continuous integrands have complex and absolute line integrals along every rectifiable path
Statement
Let be rectifiable and let be continuous on its trace. Then the complex line integral The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral and the absolute line integral The absolute line integral over a rectifiable path using its arc-length function both exist.
Facts & Assumptions
Given: A rectifiable and a continuous on its trace.
A planar path is rectifiable if and only if each coordinate function has bounded variation (A path in is rectifiable exactly when every coordinate has bounded variation).
The arc-length function of a rectifiable path is continuous and nondecreasing (The arc-length function is continuous and nondecreasing, with increments equal to subpath lengths; it is strictly increasing exactly when no nondegenerate subpath is constant).
If a real integrand is continuous and a real integrator has bounded variation, then its Riemann–Stieltjes integral exists (A continuous integrand is Riemann–Stieltjes integrable against every bounded-variation integrator).
Proof
By [L1], and have bounded variation. The four real functions and are continuous, so [L3] gives all four Stieltjes integrals in the complex definition.
The function is continuous, and [L2] makes a bounded-variation integrator, so [L3] gives the absolute integral.
Thus both definitions are well-defined. On a singleton or constant path the relevant integrators are constant and every integral is .
Depends on
- The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral
- The absolute line integral over a rectifiable path using its arc-length function
- A path in $\mathbb{R}^n$ is rectifiable exactly when every coordinate has bounded variation
- The arc-length function is continuous and nondecreasing, with increments equal to subpath lengths; it is strictly increasing exactly when no nondegenerate subpath is constant
- A continuous integrand is Riemann–Stieltjes integrable against every bounded-variation integrator
Used by
- Integration over a complex chain and the index of a chain Definition
- The winding number of a closed contour about a point off its trace Definition
- Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate Lemma
- Tagged sums approximate a contour integral within oscillation times length Lemma
- Reversal negates and concatenation adds winding numbers Proposition
- Vanishing integrals around triangles construct a primitive for a continuous function on a star-shaped domain Proposition
- A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc Theorem
- A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic Theorem
- A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral Theorem
- Chain integration and the index are additive in the chain, and reverse with it Theorem
- The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours Theorem
- The integral of dz/(z-p) along a contour is the increment of a continuous logarithm Theorem
- The iterated Cauchy integral formula on a polydisc Theorem
- The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path Theorem
Cited to discharge well-definedness by The absolute line integral over a rectifiable path using its arc-length function and The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral.
Dependency tree · two levels
26 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
- L. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 (standard reference, not scraped)
- R. Howell and J. Mathews, Complex Analysis, §6.2 (standard reference, not scraped)