TheoremStatement: Literature-sourcedProof: AI-adapted

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.

The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path

Statement

Let $F$ be a primitive of a continuous function $f$ on an open set containing the trace of a rectifiable contour $γ : [a, b] \to C$ . If $F^{'} = f$ is continuous, then $\int_{γ} f (z) d z = F (γ (b)) - F (γ (a)) .$

Facts & Assumptions

Given: A rectifiable contour $γ$ and a primitive $F$ with continuous derivative $f$ . All Euclidean path statements [L2] and [L9] apply to $Φ \circ γ$ ; Complex path length equals coordinate length and piecewise speed integral transfers their chord and subpath-length assertions to $γ$ . Open balls and segments transfer by The complex coordinate isometry transports topology and affine segments. In [L4] use the coordinate straight segment and the real and imaginary components of $F \circ Φ^{- 1}$ . Their vector-integral endpoint identities recombine into the complex segment integral by For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals.

[L1]

A primitive is holomorphic and satisfies $F^{'} = f$ (A primitive of a complex function on an open set).

[L2]

Every chord is at most the length of the corresponding subpath (Every endpoint chord is no longer than the arc: $∥ γ (b) - γ (a) ∥_{2} \leq L (γ)$ ).

[L3]

A holomorphic function with continuous derivative has $C^{1}$ real and imaginary components (A holomorphic function with continuous complex derivative has $C^{1}$ real and imaginary components).

[L4]

For a $C^{1}$ real potential and a piecewise- $C^{1}$ path, the published gradient theorem gives the endpoint increment (The gradient theorem: the line integral of a gradient is the endpoint increment).

[L5]

Continuous integrands have complex line integrals along every rectifiable contour (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L6]

A closed real interval is compact, and the continuous image of a compact metric space is compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L7]

Every open cover of a compact metric space has a Lebesgue number (Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover).

[L8]

If $∣ g ∣ \leq M$ on a rectifiable contour, then $∣ \int g d z ∣ \leq M L$ (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L9]

Arc length is additive across a split of the parameter interval, including endpoint splits (Arc length is additive across every subdivision point and decreases under restriction).

[L10]

A continuous map from a compact metric space to a metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

Proof

technique · direct

1.1L1L3L6L7algebra

Fix $ε > 0$ . For a point $p$ of the trace let $S_{p}$ be the set of $r \in (0, 1]$ such that $B (p, r)$ lies in the open domain and $∣ f (u) - f (p) ∣ < ε / 2$ for every $u \in B (p, r)$ . Continuity of $f$ at $p$ and openness of the domain make $S_{p}$ nonempty, and $S_{p}$ is downward closed in $(0, 1]$ , so $r_{p} : = \frac{1}{2} \sup S_{p}$ is a positive real belonging to $S_{p}$ ; the assignment $p \mapsto r_{p}$ is defined outright, not selected, so no choice principle is used. The balls $B (p, r_{p})$ cover the compact trace by [L6], so [L7] supplies $δ > 0$ such that any two trace points at distance below $δ$ lie in a single $B (p, r_{p})$ . That ball is convex, so the segment joining them stays inside it, and $∣ f (u) - f (z) ∣ < ε$ all along that segment.

2.1step 1.1L3L4L8

For trace points $z, w$ as in step 1.1, apply [L4] componentwise to the straight segment and then [L8] to $f - f (z)$ . This gives $F (w) - F (z) = f (z) (w - z) + r (z, w)$ with $∣ r (z, w) ∣ \leq ε ∣ w - z ∣$ .

3.1step 2.1L2L5L6L9L10choose

By [L6] and [L10], choose $η > 0$ so that every partition with mesh below $η$ has consecutive trace points within $δ$ . For every such partition, sum the identity of step 2.1: the left side telescopes to $F (γ (b)) - F (γ (a))$ , and by [L2] and repeated use of [L9] the total remainder is at most $ε L (γ)$ . As the mesh tends to $0$ , [L5] identifies the limit of the main sums with the complex integral, so $∣ F (γ (b)) - F (γ (a)) - \int_{γ} f d z ∣ \leq ε L (γ)$ .

4.1step 3.1L2∎

Letting $ε ↓ 0$ proves the formula for every rectifiable contour. The argument also covers constant paths, for which [L2] gives length $0$ and both sides vanish.

Depends on

Dependency tree · 2 levels

Sources

A. Weber, Lecture Notes in Complex Analysis, §1.7