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.
ML estimate: a contour integral is bounded by a supremum bound times path length
Statement
If on the trace of a rectifiable contour , with , then
Facts & Assumptions
Given: A continuous with on a rectifiable contour .
The fundamental inequality bounds the complex integral by the absolute line integral (The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours).
The arc-length function satisfies (The arc-length function of a rectifiable path).
The Stieltjes integral bound gives under (The total-variation bound for a Riemann–Stieltjes integral).
For piecewise- paths, published scalar and vector line integrals obey the bound (Line-integral estimates by arc length and the supremum of the field).
Proof
Apply [L3] to and the nondecreasing ; by [L2], .
Combine step 1.1 with [L1].
This agrees with the published piecewise- estimate [L4] on its exact domain and extends it to rectifiable contours. The cases and give zero directly.
Depends on
- The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours
- The arc-length function $s_\gamma(t)=L(\gamma|_{[a,t]})$ of a rectifiable path
- The total-variation bound for a Riemann–Stieltjes integral
- Line-integral estimates by arc length and the supremum of the field
Used by
- Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle Corollary
- The index of a cycle is locally constant off its trace and vanishes far from it Corollary
- ML bounds for rational integrands on a semicircular arc and a line segment Example
- Cauchy estimates on a smaller concentric disc Lemma
- Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate Lemma
- Dixon's glued function is entire and vanishes at infinity Lemma
- Tagged sums approximate a contour integral within oscillation times length Lemma
- 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 uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral Theorem
- Cauchy estimates for mixed derivatives on a polydisc Theorem
- Goursat's triangle theorem remains valid for a continuous function holomorphic away from one point Theorem
- Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain Theorem
- Spectral radius formula Theorem
- The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path Theorem
- The winding number is constant on each connected component of the complement of the trace Theorem
- The winding number vanishes on the unbounded component of the complement of the trace Theorem
Dependency tree · two levels
22 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
- R. Howell and J. Mathews, Complex Analysis, §6.2 (standard reference, not scraped)