Alphabeta Math
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.

✓ 12 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Improper and Parameter-Dependent Multiple Integrals

1 · Prerequisites

2 · Summary

Riemann integration on compact Jordan sets, Fubini, and compact change of variables provide the proper integrals used on each truncation. The one-variable improper-integral theory supplies comparison and tail estimates, while the fundamental theorem of calculus and the mean value theorem control parameter difference quotients on compact cores.

Compact Jordan exhaustions define nonnegative improper multiple integrals and show that signed exhaustion-independent convergence is absolute. An integrable dominator gives uniform tail control, from which continuity and differentiation under a parameter-dependent integral follow. A bounded integrand may be changed on a content-zero set without changing its Riemann integral. This licenses recombining injective polar half-annuli across their seams; full annuli pass to compact discs, and the expanding discs evaluate the plane Gaussian integral as π, giving the positive one-dimensional value π.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-21Open item page →

Compact Jordan exhaustions of open subsets of Rn

Definition

Let n≥1 and let D⊆Rn be open. A compact Jordan exhaustion of D is a sequence (Kj)j∈N such that:

  1. every Kj⊆D is compact (Open cover, subcover, compact metric space, and compact subset of a metric space) and Jordan measurable (Jordan inner and outer content and Jordan measurable bounded sets in Rm);
  2. Kj⊆int⁡Kj+1 for every j (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space);
  3. D=⋃j∈NKj.

These clauses imply compact cofinality: every compact C⊆D is contained in some Kj. Indeed, the open sets int⁡Kj+1 cover C; compactness gives a finite subcover, and nesting places all of C in the member with largest index. For D=∅, the constant sequence Kj=∅ is an exhaustion.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Every open subset of Rn admits a compact Jordan exhaustion

Statement

Every open subset of Rn has a compact Jordan exhaustion.

Facts & Assumptions

Given: A natural n≥1 and an open set D⊆Rn.

[L1]

If C⊆U⊆Rn, where C is compact and U is open, then a compact Jordan set K, which may be a finite union of closed grid rectangles, satisfies C⊆int⁡K⊆K⊆U (A compact subset of an open Euclidean set has a compact Jordan neighborhood inside that open set).

[L2]

For a nonempty set A in a metric space, ∣d(x,A)−d(y,A)∣≤d(x,y) (∣d(x,A)−d(y,A)∣≤d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz).

[L3]

The rationals are countably infinite (Q is countably infinite).

[L4]

If C is at most countable and m∈N, then Cm is at most countable (Every finite power of an at most countable set is at most countable).

[L5]

Every nonempty subset of N has a least element (The well-ordering principle).

[L6]

Recursion on N produces a sequence from a seed and a specified successor function (The recursion theorem).

[L9]

Jordan content is defined from finite rectangular inner families and outer covers, and the empty set has content zero (Jordan inner and outer content and Jordan measurable bounded sets in Rm).

[L10]

A closed box has volume equal to the product of its side lengths (Axis-parallel rectangles in Rm and their volume).

[L11]

There is an explicit bijection N×N→N (N×N≈N).

Proof

technique · constructive
1.1L7L9L10construct

If D=∅, take Kj=∅ for all j; [L9] verifies the Jordan clause. If D=Rn, take Kj=[−(j+1),j+1]n; [L7], [L9], and [L10] make these compact Jordan boxes. Both sequences are exhaustions, and the radii begin at 1.

1.2L2L7construct

Suppose D is proper and nonempty, put F:=Rn∖D, and define Cj:={x∈Rn:∣xk∣≤j+1 for every k<n, d(x,F)≥1/(j+1)}. By [L2], each Cj is closed and bounded, hence compact by [L7], lies in D, and satisfies Cj⊆Cj+1.

1.3L3L4L11

Fix a bijection from Q to N using [L3]. Iterating the explicit pairing in [L11] codes every finite rational endpoint list by one natural, with its length included in the code; [L4] verifies each fixed-length stage. Thus all finite unions of closed rational grid rectangles admit one fixed enumeration by natural-number codes without Countable Choice.

2.1step 1.2step 1.3L1L5L8construct

Apply [L1] to C0⊆D. Its finite grid union has a positive margin between the compact core and the complement of its interior and between the union and Rn∖D. By [L8], move each of its finitely many grid endpoints by less than that margin to rational endpoints, preserving C0⊆int⁡K0⊆K0⊆D. Thus the candidate codes of step 1.3 are nonempty, and [L5] selects their least member. The same argument applied to the compact set Cj+1∪K defines a single-valued successor K′ with Cj+1∪K⊆int⁡K′⊆K′⊆D.

3.1step 1.3step 2.1L6construct

Apply [L6] to the seed (0,K0) and the successor rule of step 2.1. The second coordinates form compact Jordan sets with Cj⊆Kj⊆int⁡Kj+1⊆D.

4.1step 1.2step 3.1L7discharge-construct∎

If C⊆D is compact, [L7] bounds all of its coordinates. Also, open balls contained in D cover C; a finite subcover and the minimum of their halved radii give a positive lower bound for d(x,F) on C. Hence C⊆Cj⊆Kj for some j; in particular every point of D is eventually included, and (Kj) is an exhaustion.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Improper multiple integrals and absolute convergence on open sets

Definition

Let D⊆Rn be open. A function f:D→R is locally Riemann integrable when its restriction to every compact Jordan set K⊆D is Riemann integrable.

For nonnegative f, its improper integral is the extended-real supremum of its compact Jordan integrals.

∫Df:=sup⁡{∫Kf:K⊆D is compact and Jordan measurable}∈[0,+∞].

The supremum exists in R‾ by Every subset of R‾ has a least upper bound and a greatest lower bound in R‾, agreeing with the real supremum and infimum on nonempty sets bounded in R and includes the empty compact set, whose integral is 0.

For a signed locally Riemann-integrable f, set f+:=(∣f∣+f)/2 and f−:=(∣f∣−f)/2. These functions are locally integrable by the absolute-value and linearity clauses of Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm, and ∣f∣=f++f−. The function f is absolutely improperly integrable when ∫D∣f∣<+∞. A locally Riemann-integrable signed function is improperly integrable precisely when the nonnegative improper integral of its absolute value is finite. In that case define

∫Df:=∫Df+−∫Df−,

a difference of finite real numbers. Thus this exhaustion-independent signed convention has no +∞−(+∞) branch.

Remarks

Conditional one-variable improper integrals use a fixed order of approach to their endpoints. The definition here instead requires independence from compact Jordan exhaustions, so signed integrability is absolute in every dimension.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

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→[0,∞) is locally Riemann integrable and (Kj) is a compact Jordan exhaustion, then

∫Df=sup⁡j∈N∫Kjf.

Facts & Assumptions

Given: An open D⊆Rn, a locally Riemann-integrable f≥0, and a compact Jordan exhaustion (Kj).

[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≤g implies ∫f≤∫g (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[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 Rn).

Proof

technique · direct
1.1L1L2L3

Since Kj⊆Kj+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 ∫Kjf increasing, and every one is bounded above by the defining supremum ∫Df of [L1].

1.2L1L2L3L4

Every compact Jordan set K⊆D lies in some Kj by [L4]. Extending the two restrictions by zero to one bounding rectangle and applying [L2] and [L3] gives ∫Kf≤∫Kjf≤sup⁡i∫Kif.

2.1step 1.1step 1.2L1∎

Taking the supremum over all compact Jordan K in step 1.2 gives ∫Df≤sup⁡i∫Kif, while step 1.1 gives the reverse inequality; equality follows, including when the value is +∞.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Absolute convergence makes signed improper multiple integrals independent of exhaustion

Statement

Let f:D→R be locally Riemann integrable. If ∫D∣f∣<+∞, then for every compact Jordan exhaustion (Kj),

∫Df=lim⁡j→∞∫Kjf,

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→R, and a compact Jordan exhaustion (Kj).

[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 Rm).

[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.1L1L2L3L4

Since 0≤f+,f−≤∣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 ∫Kjf+→∫Df+ and ∫Kjf−→∫Df− along every exhaustion.

2.1step 1.1L3L4

On each compact Kj, extend the three restrictions by zero to one bounding rectangle. The identity f=f+−f− and linearity in [L3], interpreted through [L4], give ∫Kjf=∫Kjf+−∫Kjf−.

3.1step 1.1step 2.1L2∎

Subtracting the two finite limits in step 1.1 and using step 2.1 yields ∫Kjf→∫Df+−∫Df−=∫Df, independently of the exhaustion; the converse is the defining condition in [L2].

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Comparison and absolute comparison tests for improper multiple integrals

Statement

For locally integrable 0≤f≤g, comparison on compact subsets gives the same inequality for improper integrals:

0≤∫Df≤∫Dg.

If ∣f∣≤g and ∫Dg<+∞, then f is absolutely improperly integrable.

Facts & Assumptions

Given: An open set D and locally Riemann-integrable functions with the pointwise inequalities in the Statement.

[L1]

Every compact Jordan exhaustion computes a nonnegative improper integral (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[L2]

A 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]

Proper Riemann integrals on a nondegenerate rectangle preserve pointwise inequalities (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[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.1L1L3L4

On every compact Jordan K⊆D, extend f∣K and g∣K by zero to one bounding rectangle. Their zero extensions satisfy the same pointwise inequalities, so [L3] and [L4] give 0≤∫Kf≤∫Kg; taking the defining suprema, equivalently using [L1] on any exhaustion, gives 0≤∫Df≤∫Dg.

2.1step 1.1L2∎

If ∣f∣≤g and ∫Dg is finite, step 1.1 applied to ∣f∣ gives ∫D∣f∣≤∫Dg<+∞, so [L2] gives absolute improper integrability of f.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Parameter-dependent improper multiple integrals

Definition

Let D⊆Rn be open, let I⊆R be an interval, and let f:D×I→R. For t∈I, write ft(x):=f(x,t). If every slice ft is locally Riemann integrable and absolutely improperly integrable in the sense of Improper multiple integrals and absolute convergence on open sets, then

F(t):=∫Df(x,t) dx

defines the parameter-dependent improper multiple integral of f on I.

Local domination near t0∈I means that some relative neighborhood J⊆I of t0 and some nonnegative improperly integrable g:D→R satisfy ∣f(x,t)∣≤g(x) for all x∈D and t∈J.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

An integrable dominator gives uniform tail control on every compact parameter set

Statement

An integrable dominator gives one compact Jordan core outside which every dominated slice has uniformly small integral.

Precisely, let D⊆Rn be open, let I⊆R be an interval, and let f:D×I→R have locally Riemann-integrable slices ft. Let C⊆I be compact and suppose ∣f(x,t)∣≤g(x) for x∈D and t∈C, where g≥0 is locally Riemann integrable and ∫Dg<+∞. Then every ft with t∈C, and every difference ft−fs, is absolutely improperly integrable. For every ε>0 there is a compact Jordan K⊆D such that for every s,t∈C,

∣∫Dft−∫Kft∣<ε,∣∫D(ft−fs)−∫K(ft−fs)∣<2ε.

Facts & Assumptions

Given: The functions, compact parameter set, dominator, and ε>0 of the Statement.

[L1]

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

[L2]

For locally integrable 0≤u≤v, one has ∫Du≤∫Dv; if ∣u∣≤v and ∫Dv<+∞, then u is absolutely improperly integrable (Comparison and absolute comparison tests for improper multiple integrals).

[L3]

Proper multidimensional integrals are linear, monotone, and satisfy ∣∫u∣≤∫∣u∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L4]

Every open subset of Rn has a compact Jordan exhaustion (Every open subset of Rn admits a compact Jordan exhaustion).

[L5]

For an absolutely improperly integrable function, proper integrals along every compact Jordan exhaustion converge to its improper integral (Absolute convergence makes signed improper multiple integrals independent of exhaustion).

Proof

technique · direct
1.1L1L4choose

Choose a compact Jordan exhaustion (Kj) by [L4]. Then [L1] gives ∫Kjg→∫Dg<+∞, so choose K=Kj with 0≤∫Dg−∫Kg<ε.

2.1step 1.1L1L2L3L5

For every t∈C, [L2] first makes ft absolutely improperly integrable. For every later exhaustion member Ki⊇K, [L3] applied to the zero extensions gives ∣∫Kift−∫Kft∣≤∫Kig−∫Kg. Passing to the exhaustion limits by [L1] and [L5] gives ∣∫Dft−∫Kft∣≤∫Dg−∫Kg<ε.

3.1step 2.1L1L2L3L5algebra∎

Since ∣ft−fs∣≤∣ft∣+∣fs∣≤2g, [L2] makes every difference absolutely improperly integrable, and the same [L1], [L3], and [L5] argument gives the second estimate with 2ε, uniformly for s,t∈C.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Locally dominated parameter-dependent improper multiple integrals are continuous

Statement

A locally dominated parameter-dependent improper multiple integral is continuous in the parameter.

More precisely, let f:D×I→R be continuous and suppose it is locally dominated near each parameter in the sense of Parameter-dependent improper multiple integrals. Then F(t)=∫Df(x,t) dx is continuous on I in the relative topology.

Facts & Assumptions

Given: The continuous integrand f, parameter interval I, and local domination in the Statement; fix t0∈I.

[L1]

If locally integrable slices ft on an open D satisfy ∣ft∣≤g on a compact parameter set, where g≥0 and ∫Dg<+∞, then for every η>0 one compact Jordan K⊆D satisfies ∣∫Dft−∫Kft∣<η for every such t (An integrable dominator gives uniform tail control on every compact parameter set).

[L2]

A continuous map from a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L3]

Proper multidimensional Riemann integrals are monotone and satisfy the absolute-value estimate (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L5]

An integrable nonnegative dominator makes every locally integrable dominated slice absolutely improperly integrable (Comparison and absolute comparison tests for improper multiple integrals).

[L6]

Every continuous real function on a compact Jordan set is Riemann integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

Proof

technique · direct
1.1L1L5choose

Choose a compact relative parameter neighborhood C⊆I of t0 and an integrable g dominating ∣ft∣ there. Continuity gives local integrability and [L5] gives absolute improper integrability of the slices. Given ε>0, [L1] supplies a compact Jordan core K⊆D on which both tail errors are below ε/3.

1.2L2L3L4L6

The restriction of f to the compact set K×C is uniformly continuous by [L2], while [L6] supplies all proper core integrals. Hence, for t∈C sufficiently close to t0, ∣f(x,t)−f(x,t0)∣<ε/(3(1+cont⁡K)) for every x∈K, and [L3] with [L4] makes the compact-core integral difference smaller than ε/3.

2.1step 1.1step 1.2algebra∎

Split F(t)−F(t0) into the two tail errors and the core-integral difference. Steps 1.1 and 1.2 make its absolute value smaller than ε, proving relative continuity at t0, including a one-sided parameter endpoint.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

Differentiation under an improper multiple integral under an integrable derivative bound

Statement

Let D⊆Rn be open and I⊆R be an open interval. Suppose f and ∂tf are continuous on D×I, one slice ft∗ is absolutely improperly integrable, and for every compact interval C⊆I there is a nonnegative improperly integrable gC with ∣∂tf(x,t)∣≤gC(x) for x∈D and t∈C. Then every slice is absolutely improperly integrable, the function F(t)=∫Df(x,t) dx is continuously differentiable, and

F′(t)=∫D∂tf(x,t) dx.

The parameter derivative may be passed through the improper multiple integral under an integrable uniform derivative bound.

Facts & Assumptions

Given: The domain, interval, integrand, derivative, base slice, and dominators of the Statement; fix t0∈I.

[L1]

The mean value theorem gives an interior c with h(b)−h(a)=h′(c)(b−a) for a continuous function differentiable inside an interval (The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)).

[L2]

If locally integrable slices ut satisfy ∣ut∣≤g on a compact parameter set, where g≥0 and ∫Dg<+∞, then their improper-integral tails outside one compact Jordan core are uniformly small (An integrable dominator gives uniform tail control on every compact parameter set).

[L3]

If u:D×I→R is continuous and locally dominated near every parameter by a nonnegative improperly integrable function, then t↦∫Du(x,t) dx is continuous in the relative topology (Locally dominated parameter-dependent improper multiple integrals are continuous).

[L4]

If ∣u∣≤g and g has finite nonnegative improper integral, then u is absolutely improperly integrable (Comparison and absolute comparison tests for improper multiple integrals).

[L5]

A continuous map from a compact metric space is uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L6]

Proper multidimensional integrals are linear and satisfy ∣∫u∣≤∫∣u∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L7]

If u is absolutely improperly integrable, its proper integrals along every compact Jordan exhaustion converge to ∫Du (Absolute convergence makes signed improper multiple integrals independent of exhaustion).

Proof

technique · direct
1.1L1L4L6L7algebra

On the compact parameter interval between t∗ and any t∈I, [L1] gives ∣f(x,t)−f(x,t∗)∣≤∣t−t∗∣gC(x) pointwise. Fact [L4] makes the difference absolutely improperly integrable. Proper linearity in [L6] along one exhaustion and convergence in [L7] show that a sum of two absolutely improperly integrable functions is again absolutely improperly integrable, so ft=ft∗+(ft−ft∗) is absolutely improperly integrable.

1.2L1L2L5

For nonzero h with t0+h∈I, [L1] bounds the difference quotient qh(x):=(f(x,t0+h)−f(x,t0))/h by one integrable dominator. On a compact Jordan core, [L5] and [L1] make qh→∂tf(⋅,t0) uniformly as h→0.

2.1step 1.2L2L6L7

Use [L2] to make the tails of both qh and ∂tf(⋅,t0) uniformly small, then use the uniform convergence from step 1.2 on the core and [L6]. It follows that ∫Dqh→∫D∂tf(x,t0) dx. On every compact member of one exhaustion, proper linearity in [L6] gives ∫qh=(∫ft0+h−∫ft0)/h; applying [L7] to the three absolutely integrable functions passes this identity to D. Hence the left side is the difference quotient of F, proving the asserted derivative formula.

3.1step 2.1L3L4∎

Apply [L4] to each derivative slice and [L3] to the continuous integrand ∂tf, using the same local dominators, to see that the derivative integral is continuous in t. Thus F is C1 on I.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

Changing a bounded integrand on a content-zero set does not change its Riemann integral

Statement

Let E⊆Rm be bounded and Jordan measurable, let f,g:E→R be bounded, and suppose {x∈E:f(x)≠g(x)} has content zero. Then f is Riemann integrable over E if and only if g is, and when they are integrable their integrals are equal.

Facts & Assumptions

Given: The set and functions of the Statement, a nondegenerate bounding rectangle Q⊇E, their zero extensions f~,g~ to Q, and N:={x∈E:f(x)≠g(x)}.

[L1]

Riemann integrability over E means integrability of the zero extension on Q (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L2]

A set has content zero when every positive volume allowance admits a finite closed-cube cover within that allowance (Measure zero and content zero in Rm by countable and finite cube covers).

[L3]

If a subset of a rectangle is covered by finitely many rectangles of total volume V, then a grid exists whose cells meeting the set have total volume below V+η (A finite rectangle cover admits grid control with arbitrarily small volume excess).

[L4]

A bounded function on a nondegenerate rectangle is Riemann integrable exactly when grids can make its upper-minus-lower sum arbitrarily small (Riemann's criterion on a nondegenerate rectangle in Rm: integrability is equivalent to arbitrarily small Darboux gaps).

Proof

technique · cases
1.1L1algebra

Put h:=g~−f~. It is bounded, vanishes on Q∖N, and has some bound ∣h∣≤M.

2.1assume-case zerostep 1.1L4

In the case M=0, the function h is identically zero, hence integrable with integral zero.

2.2assume-case posstep 1.1L2L3L4choose

In the case M>0, given ε>0, [L2] covers N by finitely many cubes of total volume below ε/(4M), and [L3] gives a grid whose cells meeting N have total volume below ε/(2M). On all other cells h=0, while on a cell meeting N its oscillation is at most 2M, so the total Darboux gap is below ε. Thus [L4] makes h integrable; the bounds −M1N≤h≤M1N with the same grids force its integral to be zero.

3.1step 2.1step 2.2L5cases-exhaustive

The two cases exhaust M≥0, so h is integrable with integral zero. If f is integrable, then g~=f~+h is integrable and has the same integral by [L5].

4.1step 1.1step 3.1L5∎

Interchanging f and g applies step 3.1 to −h, proving the reverse integrability implication and the same equality of values.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The improper integral of e−x2 over R is finite and positive

Statement

The integral I=∫−∞∞e−x2 dx exists as a finite positive real number.

Facts & Assumptions

Given: The real exponential function and the mixed-improper convention on the real line.

[L2]

The improper integral ∫1∞x−p dx converges exactly when the rational p>1 (The improper p-test for rational exponents).

[L3]

For every real u, exp⁡(u)>0 and exp⁡(−u)=1/exp⁡(u) (The exponential is positive and satisfies exp⁡(−x)=1/exp⁡(x)).

[L4]

Improper integrals at −∞ and +∞ must converge separately before they are added (Improper integrals with several singular ends).

[L5]

If 0≤u≤v toward a singular end and the improper integral of v converges there, then the improper integral of u converges there (Comparison tests for improper integrals).

[L6]

The exponential function is strictly increasing on R (The exponential function is strictly increasing).

[L8]

Every continuous function on a compact interval is Riemann integrable (A continuous function on [a,b] is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L9]

A valid C1 substitution carries a convergent improper integral to the corresponding transformed improper integral (Change of variable in an improper integral).

Proof

technique · direct
1.1L1L2L3L5L9

If ∣x∣≥1, then [L1] and [L3] give 0<e−x2≤1/(1+x2)≤x−2. The p-test [L2] and comparison [L5] make the positive tail converge, and the substitution u=−x in [L9] gives the identical negative-tail estimate.

1.2L3L6L7L8

On [−1,1], the integrand is continuous and hence integrable by [L8]; [L6] gives e−x2≥e−1>0, so [L7] gives ∫−11e−x2 dx≥2e−1>0.

2.1step 1.1step 1.2L4∎

By [L4], the two finite tails and the proper middle integral combine to a finite mixed improper integral, and step 1.2 makes the total strictly positive.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

The square of the one-dimensional Gaussian integral is the plane Gaussian integral

Statement

Let I=∫−∞∞e−x2 dx. Then

I2=∫R2e−(x2+y2) d(x,y).

The plane integral is the nonnegative improper multiple integral.

Facts & Assumptions

Given: The finite positive number I and the nonnegative plane Gaussian.

[L1]

For continuous a and b on rectangles, ∫A×Ba(x)b(y)=(∫Aa)(∫Bb) (The integral of a product function on a product rectangle is the product of the two integrals).

[L2]

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

[L3]

The integral I=∫−∞∞e−x2 dx exists as a finite positive real number (The improper integral of e−x2 over R is finite and positive).

[L4]

The exponential satisfies exp⁡(u+v)=exp⁡(u)exp⁡(v) (The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y)).

Proof

technique · direct
1.1L1L4

For R>0, [L4] gives e−(x2+y2)=e−x2e−y2, so [L1] yields ∫[−R,R]2e−(x2+y2) d(x,y)=(∫−RRe−x2 dx)2.

2.1step 1.1L2L3

Put R=j+1. The squares form a compact Jordan exhaustion of R2, so [L2] makes their plane integrals tend to the nonnegative improper plane integral; [L3] makes each one-dimensional factor tend to I.

3.1step 2.1algebra∎

Passing to the limit in the product identity of step 1.1 gives the plane integral equal to I2.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-21Open item page →

The plane Gaussian integral equals π by polar coordinates

Statement

The nonnegative improper plane Gaussian integral satisfies

∫R2e−(x2+y2) d(x,y)=π.

Facts & Assumptions

Given: The polar map P(r,θ)=(rcos⁡θ,rsin⁡θ) and reals 0<ε<R.

[L1]

Let g be injective and C1 with invertible derivative on an open neighbourhood of a compact Jordan set K. For every bounded function f on g(K), the function f is integrable on g(K) if and only if x↦f(g(x))∣det⁡Dg(x)∣ is integrable on K, and then their integrals are equal (Change of variables for an injective C1 map on a compact Jordan set).

[L3]

Bounded functions differing only on a content-zero subset of a Jordan set are integrable simultaneously and have equal integrals (Changing a bounded integrand on a content-zero set does not change its Riemann integral).

[L4]

The graph of a continuous real function on a compact nondegenerate rectangle has content zero (The graph of a continuous function on a closed nondegenerate rectangle in Rm has content zero in Rm+1).

[L5]

A metric-bounded set is Jordan measurable if and only if its boundary has content zero (A bounded set in Rm is Jordan measurable iff its boundary is null, equivalently of content zero).

[L7]

For a Jordan set E, integrating 1E over a bounding rectangle gives cont⁡(E) (A bounded set is Jordan measurable iff its indicator is Riemann integrable, and the integral is its Jordan content).

[L8]

Proper multidimensional integrals are linear, monotone, and satisfy the absolute-value estimate (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L9]

A rectangle has volume equal to the product of its side lengths (Axis-parallel rectangles in Rm and their volume).

[L10]

The derivative of the exponential is the exponential (The exponential function is smooth and (exp⁡)′=exp⁡).

[L11]

If f:D→[0,∞) is locally Riemann integrable and (Kj) is a compact Jordan exhaustion of D, then ∫Df=sup⁡j∫Kjf (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[L12]

The derivatives of sine and cosine are cosine and negative sine (The derivatives of sine and cosine are cosine and minus sine).

[L13]

For every real θ, sin⁡2θ+cos⁡2θ=1 (Parity and the Pythagorean identity for sine and cosine).

[L14]
[L15]

One has exp⁡(x)→0 as x→−∞ (The exponential tends to +∞ at +∞ and to 0 at −∞).

[L16]

The exponential is strictly increasing (The exponential function is strictly increasing).

[L17]

The Jacobian determinant is the determinant of the derivative matrix, and change of variables uses its absolute value (The Jacobian determinant of a square-dimensional C1 map is the determinant of its Jacobian matrix).

[L18]

A continuous product function on a product rectangle has integral equal to the product of the factor integrals (The integral of a product function on a product rectangle is the product of the two integrals).

[L21]

The exponential maps R into (0,∞) and is normalized by exp⁡(0)=1 (The power-series, product-limit, IVP, functional-equation, and Picard definitions agree).

[L22]

Every continuous real function on a compact Jordan set is Riemann integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

[L23]

The pair (cos⁡θ,sin⁡θ) is injectively parametrized by 0≤θ<2π, both coordinates have period 2π, and every real number has an integer part (t↦(cos⁡t,sin⁡t) is a bijection from [0,2π) onto the real unit circle, The zero sets of sine and cosine and the least positive common period 2 pi, Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Proof

technique · direct
1.1L4L5L6L12L13L17L23algebra

On each compact rectangle [ε,R]×[0,π] and [ε,R]×[−π,0], the polar map has Jacobian determinant r(cos⁡2θ+sin⁡2θ)=r>0 by [L12], [L13], and [L17]. Enlarge the radial interval inside (0,∞) and each angular interval by less than π/2. If two points in one enlarged rectangle have the same polar image, [L13] gives equal positive radii; reducing both angles modulo 2π by [L23] and using its injective half-open parametrization shows that their difference is an integer multiple of 2π. The enlarged angular interval has length below 2π, so the angles are equal. Thus the map is injective on an open neighbourhood of each compact rectangle, and their images are the closed upper and lower half-annuli. Each half-annulus is closed and bounded, hence compact by [L6]; its boundary is contained in two continuous semicircle graphs and two radial segments, so [L4] and [L5] make it Jordan measurable.

2.1step 1.1L1L10L14L18L19L20L22

The Gaussian is continuous on each compact half-annulus and the pulled-back function e−r2r is continuous on each parameter rectangle, so [L22] supplies both integrability conditions in [L1]. Apply [L1] to each half-annulus. By [L18], the parameter-rectangle integral is π∫εRe−r2r dr. Facts [L10], [L19], and [L20] give (−12e−r2)′=re−r2, so [L14] evaluates each half as π2(e−ε2−e−R2); the lower half has the same angular length.

3.1step 1.1step 2.1L3L4L7L8

The half-annuli overlap only in the two radial boundary segments, which have content zero by [L4]. On a common bounding rectangle, 1A++1A− differs from 1A+∪A− only on that overlap, so [L3], [L7], and [L8] combine the two values from step 2.1 into the full-annulus integral π(e−ε2−e−R2).

4.1step 3.1L4L5L6

Every circle is the union of its upper and lower continuous semicircle graphs, hence has content zero by [L4]; [L5] makes every closed disc Jordan measurable, and [L6] makes it compact.

5.1step 3.1step 4.1L3L7L8L9L16L21

The omitted inner disc lies in [−ε,ε]2, whose content is 4ε2 by [L7] and [L9]. Since −(x2+y2)≤0, strict increase in [L16] and the normalization/positivity in [L21] give 0<e−(x2+y2)≤1. Thus [L8] bounds its Gaussian integral by 4ε2. The annulus and inner disc overlap only on a content-zero circle, so [L3] recombines them. Letting ε↓0 in step 3.1 gives the radius-R disc integral π(1−e−R2).

6.1step 4.1step 5.1L10L11L15L21L22∎

The closed discs of radii j+1 form a compact Jordan exhaustion of R2. The Gaussian is nonnegative by [L21], and it is locally Riemann integrable because [L10] and elementary algebra make it continuous and [L22] makes its restriction to every compact Jordan set integrable. Thus [L11], step 5.1, and [L15] show that the disc integrals tend to π, which is the improper plane integral.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21Open item page →

The Gaussian integral ∫−∞∞e−x2 dx=π

Statement

∫−∞∞e−x2 dx=π.

Facts & Assumptions

Given: Write I:=∫−∞∞e−x2 dx.

[L1]

The integral I exists as a finite positive real number (The improper integral of e−x2 over R is finite and positive).

[L2]

One has I2=∫R2e−(x2+y2) d(x,y) (The square of the one-dimensional Gaussian integral is the plane Gaussian integral).

Proof

technique · direct
1.1L1L2L3

By [L1], I>0, and [L2] with [L3] gives I2=π.

2.1step 1.1L4∎

Since I is nonnegative, uniqueness in [L4] identifies it with π.

5 · Examples, counterexamples and false statements

None yet.

Sources