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
- ML bounds for rational integrands on a semicircular arc and a line segment Example
- A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral Theorem
- The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 87 results over 21 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
- R. Howell and J. Mathews, Complex Analysis, §6.2 (standard reference, not scraped)