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.
Uniqueness of left Haar measure up to scale
Statement
Assume AC. Any two left Haar measures on an LCH group are positive scalar multiples on every Borel set.
Facts & Assumptions
Given: Left Haar measures on , and AC.
For the associated functionals, symmetric small-support functions make the comparison error arbitrarily small and have positive integrals. (Haar integral comparison inequality)
Equality on integrals identifies Radon measures on the Borel sigma algebra. (Uniqueness of the RMK representing measure among Radon measures)
Under DC, a compact set inside an open set admits a compactly supported cutoff that is one on the compact set. (LCH Urysohn cutoff)
Given a set , an element and a function , recursion gives with and . (The recursion theorem)
AC is assumed in the choice-function form stated in the cited definition. (The Axiom of Choice)
Proof
First discharge the dependent-choice hypothesis of [F3] directly. For any set , a prescribed , and a relation with every successor set nonempty, [A1] chooses one member of each set in . Composing this choice function with gives with . By [F4], and define an infinite -chain. This proves exactly the required dependent-choice principle, including the prescribed starting point. Now let and . Compact finiteness makes these real-valued on real . They are positive and invariant. They are nonzero: for each measure, nonzeroness and outer regularity give an open set of positive mass, open inner regularity gives a compact subset of positive mass, and [F3] gives a cutoff dominating its indicator. Use one such nonzero cutoff as ; strict positivity in [F1] gives .
Fix and . Choose the same symmetric so the [F1] bounds for and are both at most , using the intersection of their identity neighbourhoods. Divide by and set . Then and . Multiplying by and respectively and subtracting cancels , giving . Letting proves with .
For real , linearity extends from the positive cone to all . The measure is Radon because scaling by a finite positive scalar preserves each regularity equality and compact finiteness. Therefore [F2] gives on all Borel sets, including those of infinite measure.
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
Used by
Dependency tree · two levels
19 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
- Pedersen, Haar integral, p.2 definitions and lemma; p.3 Theorem 1; pp.4–5 second proof and Remark 2 (standard reference, not scraped)