Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-13
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.

Riemann–Lebesgue comparison for distribution test integrands

Statement

Assume Countable Choice. Let Q=∏i=1n[ai,bi] with n≥1 and ai<bi. If a bounded Borel real function f on Q is Riemann integrable, then it is Lebesgue integrable and the two integrals agree. The corresponding assertion for complex functions holds componentwise. In particular it applies to smooth compact test integrands and their bounded Borel zero extensions from compact Jordan regions.

Facts & Assumptions

[F1]

Darboux and tagged Riemann integrability agree, with the same value (The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree).

[F2]

Under Countable Choice, any set between the interior and closure of a box has its box volume as Lebesgue measure (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included).

[F3]

The nonnegative integral is monotone and homogeneous and agrees with the simple integral on nonnegative simple functions (Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions).

[F4]

Lebesgue integration is complex-linear on L1 (The Lebesgue integral is linear on L1(μ)).

[F5]

Assume The Axiom of Countable Choice (ACω), used for F2 and the Lebesgue-measure interface.

[F6]

A continuous real function on a nonempty compact metric space is bounded (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), and a compact subset of a metric space is closed (A compact subset of a metric space is closed and bounded). Riemann integration over a bounded Jordan set is defined by the zero extension to a bounding rectangle (The Riemann integral of a bounded function over a bounded Jordan measurable set), and a continuous real function on a compact Jordan set is integrable in that sense (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

Proof

Given: the bounded Borel Riemann integrand and F5.

1.1givenF2F3F5

Choose C≥0 with ∣f∣≤C, and put g=f+C≥0. F2 and F3 give ∫Q∣f∣≤Cvol⁡Q<∞ and ∫Qg≤2Cvol⁡Q<∞, so both are integrable. Borel measurability makes all these integrals defined.

2.1step 1.1F2F3

For a finite rectangular grid, list its closed cells Q1,…,Qs and set Di=Qi∖⋃j<iQj. These Borel sets partition Q, contain each cell's interior and lie in its closure, so λn(Di)=vol⁡Qi by F2. Put mi=inf⁡Qig and Mi=sup⁡Qig. The simple functions l=∑imi1Di and h=∑iMi1Di satisfy l≤g≤h everywhere, including grid faces. F3 identifies their integrals as the grid's lower and upper Darboux sums for g, so these sums bracket ∫Qg.

3.1step 2.1F1F2F4

Every tagged sum of g is the corresponding sum of f plus Cvol⁡Q. Thus g is Riemann integrable with value IR(f)+Cvol⁡Q. F1 says its supremum of lower Darboux sums and infimum of upper sums have this same value. Taking these bounds in step 2.1 squeezes ∫Qg to that value. F4 and F2 then give ∫Qf=∫Qg−Cvol⁡Q=IR(f).

4.1step 3.1F1F2F4F5F6

Apply the real result separately to the real and imaginary parts for the complex assertion; the bound ∣f∣≤∣Re⁡f∣+∣Im⁡f∣ ensures absolute integrability. For the last clause, let E⊆Q be compact Jordan and let h:E→R be continuous. If E is empty its zero extension is zero. Otherwise F6 makes h bounded, and compactness makes E closed. Its zero extension h~ is Borel: for every open O⊆R, continuity in the subspace gives h−1(O)=E∩G for some open G⊆Q; then h~−1(O)=E∩G when 0∉O, while h~−1(O)=(Q∖E)∪(E∩G) when 0∈O. The definition and theorem in F6 say exactly that this bounded zero extension is Riemann integrable on Q. The real result therefore applies; treating real and imaginary parts gives the same conclusion for continuous complex integrands, in particular smooth compact test integrands. The zero function has both integrals zero; the constant one has both integrals vol⁡Q. Degenerate boxes are excluded from this statement. No choices of tags over an infinite family were used; Countable Choice is precisely the measure hypothesis in F2. □

Depends on

Dependency tree · 2 levels

Sources