TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

Absolute convergence makes signed improper multiple integrals independent of exhaustion

Statement

Let $f : D \to R$ be locally Riemann integrable. If $\int_{D} ∣ f ∣ < + \infty$ , then for every compact Jordan exhaustion $(K_{j})$ ,

$\int_{D} f = \lim_{j \to \infty} \int_{K_{j}} f,$

and the value is independent of the exhaustion. Conversely, under the adopted definition, a signed improper multiple integral exists only under this absolute-convergence condition.

Facts & Assumptions

Given: An open set $D$ , an absolutely improperly integrable $f : D \to R$ , and a compact Jordan exhaustion $(K_{j})$ .

[L1]

Every compact Jordan exhaustion computes the nonnegative improper integral, independently of the exhaustion (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[L2]

A locally Riemann-integrable signed function is improperly integrable precisely when the nonnegative improper integral of its absolute value is finite (Improper multiple integrals and absolute convergence on open sets).

[L3]

On a nondegenerate rectangle, proper multidimensional Riemann integrals are linear and monotone (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ).

[L4]

The integral over a bounded Jordan set is the bounding-rectangle integral of the zero extension (The Riemann integral of a bounded function over a bounded Jordan measurable set).

Proof

technique · direct

1.1

Since $0 \leq f^{+}, f^{-} \leq ∣ f ∣$ , extend the restrictions to every compact Jordan set by zero on one bounding rectangle. Monotonicity in [L3], the Jordan-set definition [L4], and the defining suprema in [L2] make both nonnegative improper integrals finite; [L1] then gives $\int_{K_{j}} f^{+} \to \int_{D} f^{+}$ and $\int_{K_{j}} f^{-} \to \int_{D} f^{-}$ along every exhaustion.

L1L2L3L4

2.1

On each compact $K_{j}$ , extend the three restrictions by zero to one bounding rectangle. The identity $f = f^{+} - f^{-}$ and linearity in [L3], interpreted through [L4], give $\int_{K_{j}} f = \int_{K_{j}} f^{+} - \int_{K_{j}} f^{-}$ .

step 1.1L3L4

3.1

Subtracting the two finite limits in step 1.1 and using step 2.1 yields $\int_{K_{j}} f \to \int_{D} f^{+} - \int_{D} f^{-} = \int_{D} f$ , independently of the exhaustion; the converse is the defining condition in [L2].

step 1.1step 2.1L2∎

Depends on

Used by

Dependency tree · two levels

22 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

V. Guillemin, MIT 18.101 Analysis II Lecture Notes, Definition 3.25 (standard reference, not scraped)
M. E. Taylor, Introduction to Analysis in Several Variables, Proposition 3.1.18 (standard reference, not scraped)