Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-16
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.

For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals

Statement

Let γ:[a,b]→C be piecewise-C1 and let f be continuous on its trace. Then ∫γf(z) dz=∑j∫tjtj+1f(γ(t))γj′(t) dt, and ∫γ∣f(z)∣ ∣dz∣=∑j∫tjtj+1∣f(γ(t))∣ ∣γj′(t)∣ dt. The real and imaginary parts of the first display are the published vector line integrals of (u,−v) and (v,u), while the second is the published scalar line integral.

Facts & Assumptions

Given: A piecewise-C1 contour γ=x+iy, a continuous f=u+iv, and an admissible partition (tj).

[L1]

Let f:[a,b]→R be Riemann integrable. Suppose α is continuous on [a,b], differentiable on (a,b), and α′ extends continuously to [a,b]. Then f is Riemann–Stieltjes integrable with respect to α and ∫abf dα=∫abf(x)α′(x) dx (A continuously differentiable integrator reduces Stieltjes integration to ordinary integration).

[L2]

The published scalar and vector line integrals are the sums of ∫f(γ)∣γ′∣ and ∫⟨F(γ),γ′⟩ over the smooth pieces (Scalar line integrals with respect to arc length and vector-field line integrals).

[L3]

A piecewise-C1 path has length equal to the sum of the speed integrals, with corners and singleton intervals allowed (A continuous piecewise-C1 path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L5]

Let a<b be reals and let f:[a,b]→R be continuous. Then f is bounded and Riemann integrable on [a,b] (A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L6]

Let a<b and let γ:[a,b]→Rn be C1, and set sγ(t):=L[a,t](γ∣[a,t]). Then sγ is differentiable on [a,b] in the relative sense and sγ′(t)=∥γ′(t)∥2, the values at a and b being the relative one-sided derivatives (For a C1 path the arc-length accumulation function has derivative equal to speed).

Proof

technique · direct
1.1L1L4L5algebra

On a nondegenerate smooth piece [tj,tj+1] the integrands u(γ(t)) and v(γ(t)) are continuous, being composites of the continuous f with the continuous γ, so [L5] makes each of the four component integrands Riemann integrable; the integrators xj,yj are C1 on the piece, hence continuous with continuously extending derivative. The hypotheses of [L1] therefore hold, and applying [L1] to the four component Stieltjes integrals and recombining gives ∫f(γ(t))(xj′(t)+iyj′(t)) dt=∫f(γ(t))γj′(t) dt.

1.2L1L2L3L5L6

On the same piece the arc-length integrator is sγj, which by [L6] is differentiable with sγj′(t)=∣γj′(t)∣, continuous because γj is C1; and ∣f(γ(t))∣ is continuous, hence Riemann integrable by [L5]. So [L1] applies with α=sγj and yields ∫∣f(γ)∣ dsγj=∫∣f(γ(t))∣ ∣γj′(t)∣ dt; summing over pieces and using [L3] to identify the total arc length gives the absolute-integral formula, which is the scalar line integral in [L2].

2.1step 1.1L2

The real and imaginary parts in step 1.1 are exactly the vector line integrals of (u,−v) and (v,u) from [L2]. This uses the published real construction in a numbered step, with its piecewise-C1 hypothesis unchanged.

3.1step 1.1step 2.1step 1.2∎

Summing the identities over the pieces proves both displays. No equality of one-sided derivatives at corners is needed, and zero-speed pieces contribute 0.

Depends on

Used by

Dependency tree · two levels

58 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