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.
Existence of left and right Haar measures
Statement
Assume AC. Every LCH group has a left Haar measure representing the integral just constructed. The pushforward of this measure by inversion is a right Haar measure.
Facts & Assumptions
Given: An LCH group and AC.
A positive nonzero left-invariant functional exists under AC. (Existence of a left Haar integral)
The constructed RMK Radon measure represents a positive functional. (Positive functionals on C_c(X) are integration against a Radon measure)
Equality on all real integrals implies equality of Radon measures on all Borel sets. (Uniqueness of the RMK representing measure among Radon measures)
Translation and inversion are homeomorphisms and preserve . (Translations preserve compactly supported continuous functions)
AC covers DC and countable open approximations. (The Axiom of Choice)
The open content has the equivalent compactly supported cutoff supremum. (The RMK functional outer content is well defined)
A finite open cover of a compact set admits a nonnegative subordinate partition under DC. (A finite compactly supported partition of unity near a compact set)
Proof
Let be the integral in [F1]. At the outer-subadditivity step in its RMK construction, use the equivalent supremum in [F6] over with . If , this support has a finite subcover with distinct indices. A subordinate partition from [F7] gives , each term compactly supported in its assigned and bounded by one there, since the partition sums to one on the support of . Hence and taking the supremum gives open subadditivity. For arbitrary sets with finite sum of outer contents, choose open supersets with errors under AC. Their union gives ; infinite sums need no estimate. Letting supplies the required subadditivity. This corrects the inference from to support containment, which is not valid by itself.
With that construction step justified, [F2] represents by a Radon measure . It is nonzero because some . A homeomorphism takes compact sets to compact sets and bijects open sets and Borel sets. Therefore is finite on compact sets and inherits outer regularity and open inner regularity by transporting the approximating open and compact sets.
For , integration against gives for every real . The pushforward integral identity follows first for indicators and simple functions and then by monotone approximation of nonnegative measurable functions and positive/negative parts. RMK uniqueness now gives , hence left invariance. For inversion, put . Since , . It is nonzero and Radon by step 2.1, hence right Haar.
Sources
Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13. Local argument and conventions as displayed above.
Depends on
- Existence of a left Haar integral
- Positive functionals on C_c(X) are integration against a Radon measure
- Uniqueness of the RMK representing measure among Radon measures
- Translations preserve compactly supported continuous functions
- The Axiom of Choice
- The RMK functional outer content is well defined
- A finite compactly supported partition of unity near a compact set
Used by
Dependency tree · two levels
22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13 (standard reference, not scraped)