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
- A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral Theorem
- The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours 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 · next 3 levels
Direct dependencies and their dependencies through the next three levels: 113 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)