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.
Vanishing integrals around triangles construct a primitive for a continuous function on a star-shaped domain
Statement
Let be open and star-shaped with respect to in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification , and let be continuous. Suppose
for every filled triangle in the sense of Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter. Then
is holomorphic on and satisfies for every . Thus is a primitive of as defined in A primitive of a complex function on an open set.
Facts & Assumptions
Given: An open set star-shaped with respect to , a continuous , and vanishing boundary integral for every filled triangle contained in .
Reversal negates a contour integral and concatenation adds contour integrals (Complex line integrals change sign under reversal and add under concatenation).
On a piecewise- contour, the complex line integral agrees with the usual parametric integral (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).
Complex line integrals are linear in the integrand, and the ML estimate bounds their modulus by a uniform integrand bound times contour length (Complex line integrals are linear in the integrand, ML estimate: a contour integral is bounded by a supremum bound times path length).
A primitive of on an open set is a holomorphic function whose derivative equals there (A primitive of a complex function on an open set).
A continuous integrand has a complex line integral along every rectifiable contour (Continuous integrands have complex and absolute line integrals along every rectifiable path).
Proof
Fix . The segment is rectifiable and is continuous on it, so exists by [L5]. Since is open, choose with . If , the short segment from to lies in that ball, and every segment from to a point of the short segment lies in by star-shapedness; hence .
Parametrizing the short edge by and using [L2] gives .
The zero boundary integral of that triangle reads by [L1], and therefore .
By [L3], steps 2.1 and 1.2 imply .
Continuity of at makes the right side of step 3.1 tend to zero as . Thus for arbitrary , including ; [L4] says exactly that is a primitive, and was only the excluded difference-quotient value.
Depends on
- Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter
- Complex star-shaped and convex domains are the published Euclidean notions under the identification $\mathbb C=\mathbb R^2$
- A primitive of a complex function on an open set
- For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals
- Continuous integrands have complex and absolute line integrals along every rectifiable path
- Complex line integrals change sign under reversal and add under concatenation
- ML estimate: a contour integral is bounded by a supremum bound times path length
- Complex line integrals are linear in the integrand
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 123 results over 20 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
- Tang-Kai Lee, Complex Analysis Notes, Section 2.1.2 (standard reference, not scraped)