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.

✓ 10 results · all verified · 3 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 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Product Measures and the Fubini Tonelli Theorems — Examples

1 · Prerequisites

2 · Summary

The companion page keeps the concrete computations and failure witnesses close to the theorem chain: Gaussian and Basel-style product-integral computations first, then the sectionwise-measurable, non-sigma-finite, non-L1, nonuniqueness, incompleteness, and completion counterexamples that the A page points at.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

Tonelli and the plane polar formula give int_R e^{-x^2} dx = sqrt(pi)

Example

Let I:=∫Re−x2 dx. Then I=π.

Facts & Assumptions

Given: The nonnegative function x↦e−x2 on R.

[L1]

Tonelli's theorem applies to nonnegative functions on R2. (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product)

[L2]

The plane Gaussian integral equals π. (The plane Gaussian integral equals π by polar coordinates)

Verification

technique · direct
1.1L1

Since e−x2e−y2=e−(x2+y2) is nonnegative, Tonelli gives I2=∫R∫Re−(x2+y2) dy dx.

2.1L2step 1.1∎

By [L2], the double integral in step 1.1 is π. Since I≥0, it follows that I2=π and hence I=π.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

Tonelli and the geometric series compute int_0^1 int_0^1 1/(1-xy) dx dy = pi^2/6

Example

One has ∫01∫0111−xy dx dy=π26.

Facts & Assumptions

Given: The function (x,y)↦(1−xy)−1 on (0,1)2.

[L2]

Tonelli allows termwise summation of a nonnegative double series. (Tonelli's theorem for double series of nonnegative extended real numbers)

[A1]

The classical Basel identity is ∑n≥11n2=π26.

Verification

technique · direct
1.1L1

For (x,y)∈(0,1)2, [L1] gives 11−xy=∑n=0∞(xy)n with nonnegative terms.

2.1L2step 1.1

Tonelli and [L2] allow termwise integration: ∫01∫0111−xy dx dy=∑n=0∞(∫01xn dx)(∫01yn dy)=∑n=0∞1(n+1)2.

3.1A1step 2.1∎

Reindexing and applying [A1] yields ∫01∫0111−xy dx dy=∑m=1∞1m2=π26.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

The region under x maps to x^2 on [0,1] has measure 1/3

Example

The set R:={(x,t)∈[0,1]×R:0≤t<x2} has planar Lebesgue measure 1/3.

Facts & Assumptions

Given: The function f(x)=x2 on [0,1].

[L1]

The region under a nonnegative measurable function has product measure equal to its integral. (The region under a nonnegative measurable function is product-measurable and has measure equal to the integral)

Verification

technique · direct
1.1

Applying [L1] to f(x)=x2 gives [L1] λ2(R)=∫01x2 dx.

2.1

Since (x3/3)′=x2, [L2] gives [L2, step 1.1] λ2(R)=∫01x2 dx=13. ∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

Cavalieri computes the area of the unit disc from its sections

Example

Let D:={(x,y)∈R2:x2+y2<1}. Then λ2(D)=∫−1121−x2 dx=π.

Facts & Assumptions

Given: The unit disc D⊆R2.

[L1]

Tonelli computes the area of a measurable set from the lengths of its sections. (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product)

[L2]

The unit ball in R2 has area π. (The closed form for the volume of the unit n-ball)

Verification

technique · direct
1.1L1

For x∈[−1,1], the vertical section of D is Dx=(−1−x2,1−x2), so λ1(Dx)=21−x2; outside [−1,1] the section is empty. Applying [L1] to 1D therefore gives λ2(D)=∫−1121−x2 dx.

2.1L2step 1.1∎

The same set D is the unit ball in R2, so [L2] gives ∫−1121−x2 dx=λ2(D)=π.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

A set can have measurable horizontal and vertical sections and still fail to be product-measurable

Statement refuted

If E⊆X×Y has measurable horizontal and vertical sections for every parameter, then E is product-measurable.

Counterexample

technique · direct

Assume the Axiom of Countable Choice. Let X be the set of countable ordinals, let M be the sigma-algebra of countable and cocountable subsets of X, and define E:={(x,y)∈X×X:y<x}.

Facts & Assumptions

Given: The set E⊆X×X above.

[L1]

A sigma-algebra is closed under complements and countable unions (Sigma-algebras), and under countable choice a countable union of countable sets is countable (The Axiom of Countable Choice (ACω), Countable unions of at most countable sets, assuming ACω). Hence the countable-cocountable family on an uncountable set is a sigma-algebra.

[L2]

For sigma-finite measures, the two iterated section-measure integrals of a product-measurable set agree. (For sigma-finite measures, the two section-measure integrals of a measurable set agree)

[A1]

Define ν on M by ν(A)=0 for countable A and ν(A)=1 for cocountable A. The same countable-union argument as in [L1] shows that ν is a finite measure on (X,M).

Verification

1.1givenL1

For each x∈X, the section Ex={y:y<x} is countable by the choice of X, hence measurable for M. For each y∈X, the section Ey={x:y<x} has countable complement {x:x≤y}, hence is cocountable and measurable.

2.1A1L2step 1.1∎

Suppose for contradiction that E were product-measurable for M⊗M. Since ν(X)=1, the measure ν is finite and hence sigma-finite, so [L2] would give ∫Xν(Ex) dν=∫Xν(Ey) dν. But step 1.1 makes ν(Ex)=0 for every x and ν(Ey)=1 for every y, so the two sides are 0 and 1, a contradiction. Therefore E is not product-measurable, even though all of its sections are measurable. Thus the displayed implication is false.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

The diagonal under Lebesgue times counting measure shows that Tonelli needs sigma-finiteness

Statement refuted

Tonelli's theorem holds without any sigma-finiteness hypothesis.

Counterexample

technique · direct

Let X=Y=[0,1], let μ be Lebesgue measure on X, let ν be counting measure on Y, and let D:={(x,y)∈[0,1]2:x=y}.

Facts & Assumptions

Given: Lebesgue measure μ on [0,1], counting measure ν on [0,1], and the diagonal set D.

[A1]

For every x,y∈[0,1], the horizontal and vertical sections of the diagonal are Dx={x} and Dy={y}.

Verification

1.1givenA1

For fixed x∈[0,1], the section Dx={x} has counting measure 1, so ∫Xν(Dx) dμ(x)=∫011 dx=1.

2.1A1∎

For fixed y∈[0,1], the section Dy={y} has Lebesgue measure 0, so ∫Yμ(Dy) dν(y)=∫[0,1]0 dν=0. The iterated integrals are unequal, so Tonelli fails once the counting-measure factor is not sigma-finite.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-29Open item page →

The function (x^2-y^2)/(x^2+y^2)^2 shows that Fubini's integrability hypothesis is not decorative

Statement refuted

Fubini's theorem remains valid if one deletes the assumption f∈L1(μ×ν).

Counterexample

technique · direct

On (0,1)2, let f(x,y):=x2−y2(x2+y2)2.

Facts & Assumptions

Given: The function f above.

[L1]

The principal inverse tangent satisfies (arctan⁡u)′=11+u2 and arctan⁡u=∫0udt1+t2. (Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series)

[A1]

On (0,1)2 one has x2+y2>0, so the rational functions written below are well-defined and differentiable.

Verification

1.1A1algebra

Direct differentiation gives f(x,y)=∂y(yx2+y2)=−∂x(xx2+y2).

2.1step 1.1L1

Integrating the first identity of step 1.1 in y from 0 to 1 gives ∫01f(x,y) dy=11+x2. Integrating in x and applying [L1] yields ∫01(∫01f(x,y) dy)dx=∫01dx1+x2=π4.

3.1step 1.1step 2.1L1∎

Repeating the same calculation with the second identity of step 1.1 gives ∫01(∫01f(x,y) dx)dy=−∫01dy1+y2=−π4. Therefore the iterated integrals exist and are unequal, so the conclusion of Fubini fails. In particular f∉L1((0,1)2), because otherwise Fubini's theorem for L^1 functions on a sigma-finite product would force them to agree.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Equal iterated integrals still do not imply product integrability

Statement refuted

If both iterated integrals of a function exist and are equal, then the function must belong to L1(μ×ν).

Counterexample

technique · direct

Let f(x,y):=x2−y2(x2+y2)2 on (0,1)2, and define g on ((0,1)×{0,1})×(0,1) by g((x,0),y):=f(x,y),g((x,1),y):=f(y,x). Give (0,1)×{0,1} the product of Lebesgue measure with counting measure on {0,1}, and give (0,1) Lebesgue measure.

Facts & Assumptions

Given: The function g above.

[L1]

The function f from The function (x^2-y^2)/(x^2+y^2)^2 shows that Fubini's integrability hypothesis is not decorative has two existing iterated integrals equal to π/4 and −π/4, and it is not in L1.

Verification

1.1L1

The first copy of g contributes the two iterated values of f, while the second copy contributes the same values with the order reversed. Therefore both iterated integrals of g exist and are equal to π/4+(−π/4)=0.

2.1L1step 1.1∎

The absolute integral of g is the sum of the absolute integrals of the two copies, so it is still infinite because each copy carries the non-L1 singularity of [L1]. Thus equal iterated integrals do not imply L1-integrability.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29Open item page →

Without sigma-finiteness, the rectangle formula need not determine a unique product measure

Statement refuted

The rectangle formula determines at most one product measure even without sigma-finiteness.

Counterexample

technique · direct

Let μ be Lebesgue measure on [0,1], let ν be counting measure on [0,1], let D:={(x,y)∈[0,1]2:x=y}, and let ρ,τ be the two measures on the product sigma-algebra supplied by the standard non-sigma-finite Lebesgue/counting construction in the listed Tao source.

Facts & Assumptions

Given: Lebesgue measure μ on [0,1], counting measure ν on [0,1], and the diagonal D:={(x,y)∈[0,1]2:x=y}.

[L1]

The listed Tao source's standard non-sigma-finite Lebesgue/counting construction yields measures ρ,τ on the product sigma-algebra such that ρ(A×B)=μ(A)ν(B)=τ(A×B) on measurable rectangles and ρ(D)=1≠0=τ(D).

Verification

1.1L1

By [L1], ρ and τ agree on every measurable rectangle.

2.1L1step 1.1∎

The same fact [L1, step 1.1] gives ρ(D)=1≠0=τ(D), so the two measures are distinct. Therefore the rectangle formula does not determine a unique product measure without sigma-finiteness.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-09-08 (Codex)Open item page →

A nonmeasurable subset of a null line shows that the product of complete measures need not be complete

Statement refuted

Assuming the Axiom of Countable Choice, the product of two complete measure spaces is always complete.

Counterexample

technique · direct

Assume AC. Take a Vitali set V⊆[0,1] and put E:={0}×V⊆R2. The two factors are complete Lebesgue measure spaces, but their product is not complete. The verification supplies the witness using AC, not countable choice alone.

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice). Write λ for Lebesgue measure on L(R).

[L1]

Every section of a product-measurable set is measurable. (Every section of a product-measurable set is measurable)

[L3]

For sigma-finite factors, the product measure satisfies the rectangle formula. (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique)

[L4]

Assuming countable choice, the intervals {0}=[0,0] and [0,1] are Lebesgue measurable with measures 0 and 1 respectively. (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included)

[L7]

Completeness means that every subset of a measurable null set is measurable (Complete measure spaces).

[L8]

Countable choice asks for a choice function on every sequence of nonempty sets (The Axiom of Countable Choice (ACω)).

Verification

1.1givenL6L8construct

AC implies [L8]: apply AC to the family {Xn:n∈N} of a sequence of nonempty sets and compose its choice function with n↦Xn. This supplies countable choice for [L2], [L4] and [L5]. AC also supplies the selector in [L6]; fix that Vitali set V⊆[0,1], which is non-Lebesgue-measurable, and set E={0}×V.

2.1step 1.1L2L3L4algebra

Both factors are sigma-finite by [L2]. The rectangle Z={0}×[0,1] is product-measurable and [L3] and [L4] give (λ×λ)(Z)=λ({0})λ([0,1])=0⋅1=0. Since V⊆[0,1], we have E⊆Z.

3.1step 1.1step 2.1L1L5L7∎

If E belonged to L(R)⊗L(R), then [L1] would make E0={y:(0,y)∈E}=V Lebesgue measurable, contrary to step 1.1. Thus the subset E of the measurable null set Z is not product-measurable. By [L7] the product is not complete, although [L5] makes both factors complete.

CounterexampleConstruction: AI-adaptedVerification: AI-generatedverified 2026-09-23 (gpt-6-sol)Open item page →

A completed-product measurable set can have a nonmeasurable exceptional section

Statement refuted

Assuming the Axiom of Choice, the assertion that every section of a completed-product measurable function is measurable is false.

Counterexample

technique · direct

Apply AC to the nonempty equivalence classes of x∼y  ⟺  x−y∈Q on [0,1], selecting one point from each class. This gives a Vitali set N⊆[0,1] as in Vitali set on [0,1], and Assuming the Axiom of Choice, a Vitali set is not Lebesgue measurable proves that N is not Lebesgue measurable. Let E:={0}×N⊆R2. Put f:=1E.

Facts & Assumptions

Given: The function f=1E above.

[L1]

The set E={0}×N is contained in a planar null set, so it becomes measurable after completing the product measure. (A nonmeasurable subset of a null line shows that the product of complete measures need not be complete)

[A1]

The Axiom of Choice supplies the Vitali selector in the construction above; the same AC premise covers the Lebesgue-measure contracts used by [L1] and the Vitali nonmeasurability theorem.

Verification

1.1A1L1

By [A1] and [L1], the indicator f is measurable for the completed product measure.

2.1step 1.1∎

The section at 0 is f0=1N, whose support N is not Lebesgue measurable. Hence f0 is not measurable. So completed-product measurability gives section measurability only almost everywhere, not at every parameter.

Sources