Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

The one-dimensional torus and its normalized Haar integral

Definition

Throughout, assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Lebesgue measure on Rn is written λn (Lebesgue measurable sets, the family L(Rn), and the restricted set function λn), and Z⊆R is the copy of the integers (The integers as equivalence classes of pairs of naturals).

The torus. Let q:R→T:=R/Z be the canonical projection of the quotient of the additive group R by its subgroup Z, carrying the quotient topology (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison); we write [t]:=q(t)=t+Z. Thus [s]=[t] exactly when s−t∈Z. The map q is continuous (Continuity of a map of topological spaces at a point and globally), and T is a compact Hausdorff space homeomorphic to the Euclidean unit circle.

Fundamental domain. Every class has exactly one representative in [0,1): for t∈R the integer part n=⌊t⌋ satisfies n≤t<n+1, so t−n∈[0,1) represents [t] (Integer part: for every real x there is exactly one integer m with m≤x<m+1); and if s,t∈[0,1) satisfy s−t∈Z, then ∣s−t∣<1 forces s=t. Consequently the map [0,1)→T, t↦[t], is a bijection.

Topological checks. The closed interval [0,1] is compact by Heine-Borel by bisection: every closed bounded interval [a,b] is compact and maps onto T, so the quotient is compact by A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism. The map t↦(cos⁡2πt,sin⁡2πt) is continuous by The derivatives of sine and cosine are cosine and minus sine and A function differentiable at c is continuous at c, and is constant on quotient fibres by The zero sets of sine and cosine and the least positive common period 2 pi. It induces a continuous map φ:T→S1 by For a quotient map q:X→Y, a map out of Y is continuous iff its composite with q is; a continuous map on X constant on the fibres of q factors uniquely through q; and a composite of quotient maps is a quotient map. The bijection of [0,2π) with the circle in t↦(cos⁡t,sin⁡t) is a bijection from [0,2π) onto the real unit circle, together with the unique representatives in [0,1), makes φ bijective. The Euclidean circle is Hausdorff by Distinct points of a metric space have disjoint balls around them, so the compact-to-Hausdorff clause of A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism makes φ a homeomorphism. In particular T is Hausdorff.

The map q is open: for an open U⊆R, its saturation q−1[q[U]]=⋃k∈Z(U+k) is open. The images under q of rational-endpoint open intervals form a countable base: if q(t)∈V with V open, choose such an interval containing t and contained in q−1[V]. Its image is an open neighbourhood contained in V.

The measure. For a Borel set E∈B(T) (The Borel sigma-algebra of a topological space) the preimage q−1[E] is a Borel subset of R, because q is continuous (A continuous map has Borel preimages of Borel sets), hence Lebesgue measurable (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable). Define

mT(E):=λ1(q−1[E]∩[0,1)),

the value at q−1[E] of the same-ambient restriction of λ1 to [0,1) (Restriction of a measure to a measurable set).

This is a measure on B(T) by The restriction of a measure to a measurable set is a measure: the assignment E↦λ1(q−1[E]∩[0,1)) is the composition of the restriction measure with the inverse image along q, and inverse images preserve the empty set, complements and countable unions, while countable additivity is that of λ1. It is a probability measure: mT(T)=λ1([0,1))=1 (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included). Thus (T,B(T),mT) is a probability measure space (Measure spaces, Measures on sigma-algebras).

The integral. For a Borel measurable F:T→[0,+∞], define

∫TF dmT:=∫[0,1)F∘q dλ1.

The defining integral is meaningful because F∘q is Borel (Composition with a Borel measurable outer map preserves measurability, A continuous map has Borel preimages of Borel sets). The assignment agrees with E↦mT(E) on indicators, and it is additive and homogeneous on finite nonnegative simple functions; for a sequence 0≤F0≤F1≤⋯ with Fn↑F pointwise the identity passes to the limit because Fn∘q↑F∘q and monotone convergence holds for λ1 (Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral). For real or complex integrable F the integral is defined by decomposition into nonnegative parts or into real and imaginary parts, and it is linear (Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on L1(μ)). In particular ∫T1 dmT=1, and the same formula holds with [0,1) replaced by any half-open interval [a,a+1) or (a,a+1], by the periodicity of q−1[E] and the translation invariance of λ1 (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

Translation invariance. For y∈R the map τy:T→T, τy([t]):=[t+y], is well defined (if s−t∈Z then (s+y)−(t+y)∈Z) and continuous, because it is induced by the continuous map t↦q(t+y) from R to T. This composite is constant on the fibres of q, since q(t)=q(s) implies q(t+y)=q(s+y) (For a quotient map q:X→Y, a map out of Y is continuous iff its composite with q is; a continuous map on X constant on the fibres of q factors uniquely through q; and a composite of quotient maps is a quotient map). It preserves mT: write y=n+r with n=⌊y⌋ and r∈[0,1), put A:=q−1[E] and use that A−n=A and that A∩[0,1)=(A∩[0,r))∪(A∩[r,1)) while A∩[r,r+1)=(A∩[r,1))∪((A∩[0,r))+1), so that

mT(τy−1E)=λ1((A−y)∩[0,1))=λ1(A∩[r,r+1))=λ1(A∩[0,1))=mT(E),

the middle equality by translation invariance of λ1. Hence (T,B(T),mT,τy) is a measure-preserving system for every y, and the published integral-invariance theorem gives ∫TF∘τy dmT=∫TF dmT for every measurable F≥0 and every integrable F (Measure-preserving transformations and systems, Integral invariance under measure-preserving maps). This is the normalized Haar integral of T; abstract Haar theory is not invoked.

The finite torus. For a natural n≥1 put Tn:=Rn/Zn with the quotient topology of the canonical projection qn, and define

mTn(E):=λn(qn−1[E]∩[0,1)n),∫TnF dmTn:=∫[0,1)nF∘qn dλn.

Coordinatewise integer parts give unique representatives in [0,1)n, and the continuous quotient map sends the compact cube [0,1]n onto Tn. Compactness of the cube follows from Heine-Borel by bisection: every closed bounded interval [a,b] is compact and A product of finitely many compact spaces is compact in the product topology, and compactness of its image follows from A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism. Preimages of Borel sets are Borel; disjoint preimages and countable additivity make the displayed set function a measure, and the box formula gives total mass one. The integral identity follows from indicators, increasing simple approximation and decomposition exactly as in one dimension. For translation invariance, discard the integer parts of the translation vector, split each coordinate of [0,1)n at its fractional part, and translate the resulting 2n disjoint half-open boxes by integer vectors to partition the translated cube. The periodic preimage set is unchanged by these integer vectors; finite additivity and Lebesgue translation invariance give the same measure. Applying the indicator identity, simple approximation and decomposition gives the integral formula on any translated cube. The coordinate projections induce a continuous bijection Φ:Tn→(R/Z)n by the universal property. Its domain is compact by the preceding check, while its codomain is a finite product of Hausdorff spaces and hence Hausdorff (Arbitrary products preserve T0, T1, and Hausdorffness); the continuous-bijection theorem therefore makes Φ a homeomorphism. Thus Tn carries the finite product topology (The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A product of finitely many compact spaces is compact in the product topology, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism), and its characters x↦exp⁡(2πi k⋅x), k∈Zn, are defined on this compact Hausdorff space: replacing representatives by integer vectors leaves the exponential unchanged by exp⁡(x+iy)=ex(cos⁡y+isin⁡y), ∣exp⁡(x+iy)∣=ex, and eiπ+1=0 and the trigonometric period. Finite products of the countable base above form a countable rectangular base. Hence every product-open set is a countable union of Borel rectangles. Conversely coordinate projections are continuous, so Borel rectangles are Borel in the product. Thus the product Borel sigma-algebra equals the Borel sigma-algebra of Tn. On a product A0×⋯×An−1 of Borel subsets of the factors, the defining fundamental-domain formula and repeated application of On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n} give mTn(A0×⋯×An−1)=∏jmT(Aj), so mTn agrees on every measurable rectangle with the product measure mT×⋯×mT (The product measure of two sigma-finite measure spaces); both are probability measures, and uniqueness of the product measure on sigma-finite spaces identifies them on the entire Borel sigma-algebra (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique). Fubini's theorem then computes iterated integrals of L1 functions on Tn (Fubini's theorem for L^1 functions on a sigma-finite product).

Depends on

Dependency tree · 2 levels

Sources