Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Complex integration by parts on intervals and decaying lines

Statement

Assume countable choice. For complex C1 functions u,v on [a,b], a<b, Lebesgue integration gives abuv=u(b)v(b)u(a)v(a)abuv and abu=u(b)u(a). If instead u,vC1(R;C), uv,uvL1(R) and u(x)v(x)0 as x±, then Ruv=Ruv.

Facts & Assumptions

Given: The stated functions, The Axiom of Countable Choice (ACω), and the componentwise calculus/integration convention of Complex Lp classes and Euclidean test-function conventions.

[F2]

A bounded Riemann integrable real function on a closed interval has the same Lebesgue integral under countable choice (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[F4]

Dominated convergence applies to complex integrable functions (Dominated convergence).

Proof

1.1

Write u=r+is, v=p+iq. Apply F1 to the four real pairs (r,p),(s,q),(r,q),(s,p). Subtract the second identity from the first and add i times the sum of the last two. Since uv=(rpsq)+i(rq+sp) and uv=(rpsq)+i(rq+sp), the result is the complex integration-by-parts identity. All integrands are continuous on the compact interval and hence bounded and Riemann integrable; F2 changes each real integral to a Lebesgue integral. Applying F3 to r,s and the same F2 gives the complex FTC. This is the sole countable-choice use here.

F1F2F3given
2.1

For the whole-line assertion apply step 1.1 on [N,N]. The truncated products converge pointwise to uv and uv and have integrable majorants uv and uv. F4 gives convergence of both integrals; the boundary term u(N)v(N)u(N)v(N) tends to zero by the two assumed limits. Passing to the limit proves the assertion. No separate integrability of u or v is required.

F4step 1.1given

Depends on

Used by

Dependency tree · two levels

60 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