Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Compactly supported kernels admit commuting radon integrals

Statement

Assume AC. Let X,Y be LCH spaces and I,J positive real-linear functionals on Cc(X),Cc(Y). For real F∈Cc(X×Y), the partial integrals are continuous and compactly supported, and IxJyF(x,y)=JyIxF(x,y). Complexification gives the same identity for complex kernels.

Facts & Assumptions

Given: X,Y,I,J,F as stated, with AC.

[F1]

Support is the closure of the nonzero locus. (Compact support, Cc(X), and C0(X))

[F2]

A finite open cover of a compact set has a nonnegative compactly supported subordinate partition under DC. (A finite compactly supported partition of unity near a compact set)

[F3]

Compact sets admit nonnegative compactly supported cutoffs equal to one under DC. (LCH Urysohn cutoff)

[F4]
[F6]

AC supplies the inherited cutoff and partition choices. (The Axiom of Choice)

Proof

technique · direct
1.1F1F3F5F6

Let KX,KY be the projections of supp⁡F. They are compact. If either is empty then F=0 and both partial and iterated integrals vanish. Otherwise choose 0≤cX,cY≤1 in Cc, equal to one on these projections. Write LY=supp⁡cY. All sections are continuous and supported in the respective compact projection.

2.1F4step 1.1

For fixed y0 and ϵ>0, continuity of F(x,y)−F(x,y0) at each (x,y0) gives rectangles where its absolute value is <ϵ. Take finitely many covering KX and intersect their y-neighbourhoods. The resulting section difference is bounded by ϵcX everywhere, because it vanishes outside KX. Thus ∣I(Fy)−I(Fy0)∣≤ϵI(cX). This proves continuity of the I partial integral (also if I(cX)=0); it vanishes off KY, so has compact support. Repeating the rectangle argument with x,y interchanged proves the other partial-integral assertion.

3.1F2F6step 1.1step 2.1

Take finitely many neighbourhoods Vj with centres yj covering LY and satisfying sup⁡x∣F(x,y)−F(x,yj)∣<ϵ on Vj. A partition ψj subordinate to them sums to one on LY. Put H(x,y)=cY(y)∑jψj(y)F(x,yj). Since F=cYF, on LY the convex-combination bound gives ∣F−H∣≤ϵcXcY; off LY both vanish. This also holds off KX. Each tensor factor is in the appropriate Cc.

4.1F4step 2.1step 3.1∎

Linearity gives IxJyH=∑jI(Fyj)J(cYψj)=JyIxH. Applying positivity twice to the error bound in either order yields ∣IxJyF−JyIxF∣≤2ϵI(cX)J(cY). The cutoff integrals are finite real numbers, so arbitrariness of ϵ proves equality, including either zero cutoff integral. Real and imaginary parts prove the complex claim.

Sources

Pedersen, Haar integral, p.2 definitions and lemma; p.3 Theorem 1; pp.4–5 second proof and Remark 2. Local argument and conventions as displayed above.

Depends on

Dependency tree · 2 levels

Sources