TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Every Jordan exhaustion computes a nonnegative improper multiple integral

Statement

Every compact Jordan exhaustion computes the nonnegative improper integral, independently of the exhaustion.

Precisely, if $f : D \to [0, \infty)$ is locally Riemann integrable and $(K_{j})$ is a compact Jordan exhaustion, then

$\int_{D} f = \sup_{j \in N} \int_{K_{j}} f .$

Facts & Assumptions

Given: An open $D \subseteq R^{n}$ , a locally Riemann-integrable $f \geq 0$ , and a compact Jordan exhaustion $(K_{j})$ .

[L1]

For nonnegative $f$ , its improper integral is the extended-real supremum of its compact Jordan integrals (Improper multiple integrals and absolute convergence on open sets).

[L2]

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

[L3]

The integral over a bounded Jordan set is the integral over a bounding rectangle of the function extended by zero outside that set (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L4]

Compact cofinality is part of every compact Jordan exhaustion: every compact subset of the open domain lies in some member (Compact Jordan exhaustions of open subsets of $R^{n}$ ).

Proof

technique · direct

1.1L1L2L3

Since $K_{j} \subseteq K_{j + 1}$ , extend both restricted functions by zero to one common bounding rectangle. Their zero extensions are ordered pointwise, so [L2] and [L3] make the numbers $\int_{K_{j}} f$ increasing, and every one is bounded above by the defining supremum $\int_{D} f$ of [L1].

1.2L1L2L3L4

Every compact Jordan set $K \subseteq D$ lies in some $K_{j}$ by [L4]. Extending the two restrictions by zero to one bounding rectangle and applying [L2] and [L3] gives $\int_{K} f \leq \int_{K_{j}} f \leq \sup_{i} \int_{K_{i}} f$ .

2.1step 1.1step 1.2L1∎

Taking the supremum over all compact Jordan $K$ in step 1.2 gives $\int_{D} f \leq \sup_{i} \int_{K_{i}} f$ , while step 1.1 gives the reverse inequality; equality follows, including when the value is $+ \infty$ .

Depends on

Used by

Dependency tree · two levels

23 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, Theorem 3.24 (standard reference, not scraped)