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 ()). Lebesgue measure on is written (Lebesgue measurable sets, the family , and the restricted set function ), and is the copy of the integers (The integers as equivalence classes of pairs of naturals).
The torus. Let be the canonical projection of the quotient of the additive group by its subgroup , 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 . Thus exactly when . The map is continuous (Continuity of a map of topological spaces at a point and globally), and is a compact Hausdorff space homeomorphic to the Euclidean unit circle.
Fundamental domain. Every class has exactly one representative in : for the integer part satisfies , so represents (Integer part: for every real there is exactly one integer with ); and if satisfy , then forces . Consequently the map , , is a bijection.
Topological checks. The closed interval is compact by Heine-Borel by bisection: every closed bounded interval is compact and maps onto , 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 is continuous by The derivatives of sine and cosine are cosine and minus sine and A function differentiable at is continuous at , 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 by For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map. The bijection of with the circle in is a bijection from onto the real unit circle, together with the unique representatives in , 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 is Hausdorff.
The map is open: for an open , its saturation is open. The images under of rational-endpoint open intervals form a countable base: if with open, choose such an interval containing and contained in . Its image is an open neighbourhood contained in .
The measure. For a Borel set (The Borel sigma-algebra of a topological space) the preimage is a Borel subset of , because is continuous (A continuous map has Borel preimages of Borel sets), hence Lebesgue measurable (Assuming countable choice, every Borel subset of is Lebesgue measurable). Define
the value at of the same-ambient restriction of to (Restriction of a measure to a measurable set).
This is a measure on by The restriction of a measure to a measurable set is a measure: the assignment is the composition of the restriction measure with the inverse image along , and inverse images preserve the empty set, complements and countable unions, while countable additivity is that of . It is a probability measure: (A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included). Thus is a probability measure space (Measure spaces, Measures on sigma-algebras).
The integral. For a Borel measurable , define
The defining integral is meaningful because is Borel (Composition with a Borel measurable outer map preserves measurability, A continuous map has Borel preimages of Borel sets). The assignment agrees with on indicators, and it is additive and homogeneous on finite nonnegative simple functions; for a sequence with pointwise the identity passes to the limit because and monotone convergence holds for (Every nonnegative measurable function is the increasing limit of simple measurable functions, Monotone convergence for the integral). For real or complex integrable 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 ). In particular , and the same formula holds with replaced by any half-open interval or , by the periodicity of and the translation invariance of (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).
Translation invariance. For the map , , is well defined (if then ) and continuous, because it is induced by the continuous map from to . This composite is constant on the fibres of , since implies (For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map). It preserves : write with and , put and use that and that while , so that
the middle equality by translation invariance of . Hence is a measure-preserving system for every , and the published integral-invariance theorem gives for every measurable and every integrable (Measure-preserving transformations and systems, Integral invariance under measure-preserving maps). This is the normalized Haar integral of ; abstract Haar theory is not invoked.
The finite torus. For a natural put with the quotient topology of the canonical projection , and define
Coordinatewise integer parts give unique representatives in , and the continuous quotient map sends the compact cube onto . Compactness of the cube follows from Heine-Borel by bisection: every closed bounded interval 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 at its fractional part, and translate the resulting 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 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 , , and Hausdorffness); the continuous-bijection theorem therefore makes a homeomorphism. Thus carries the finite product topology (The product set 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 , , are defined on this compact Hausdorff space: replacing representatives by integer vectors leaves the exponential unchanged by , , and 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 . On a product 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 , so agrees on every measurable rectangle with the product measure (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 functions on (Fubini's theorem for L^1 functions on a sigma-finite product).
Depends on
A product of finitely many compact spaces is compact in the product topology
A translation-invariant measure on the Borel sets of giving the unit cube measure one is the restriction of Lebesgue measure
Fubini's theorem for L^1 functions on a sigma-finite product
The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection
Integer part: for every real there is exactly one integer with
The Borel sigma-algebra of a topological space
Restriction of a measure to a measurable set
The restriction of a measure to a measurable set is a measure
Assuming countable choice, every Borel subset of is Lebesgue measurable
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Continuous functions on Euclidean spaces are Borel measurable
Composition with a Borel measurable outer map preserves measurability
Every nonnegative measurable function is the increasing limit of simple measurable functions
Monotone convergence for the integral
Integrable real and complex functions, and their integrals
The Lebesgue integral is linear on
Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation
Measure-preserving transformations and systems
Integral invariance under measure-preserving maps
The Axiom of Countable Choice ()
The integers as equivalence classes of pairs of naturals
Measures on sigma-algebras
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Continuity of a map of topological spaces at a point and globally
A continuous map has Borel preimages of Borel sets
For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map
Lebesgue measurable sets, the family , and the restricted set function
The product measure of two sigma-finite measure spaces
For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
The product set 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 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 real numbers
Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume
Measure spaces
Heine-Borel by bisection: every closed bounded interval is compact
is a bijection from onto the real unit circle
The zero sets of sine and cosine and the least positive common period 2 pi
The derivatives of sine and cosine are cosine and minus sine
A function differentiable at is continuous at
Distinct points of a metric space have disjoint balls around them
Arbitrary products preserve , , and Hausdorffness
On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}
, , and