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.
Haar measure is positive on nonempty open sets and finite on compact sets
Statement
Every left Haar measure is positive on every nonempty open set and finite on every compact set, and is locally finite. Every left Haar integral is strictly positive on every nonzero nonnegative function.
Facts & Assumptions
Given: A Haar measure or Haar integral on an LCH group.
Haar objects are nonzero and left invariant; measures are compact-finite and regular. (Left Haar integral and left Haar measure)
A nonnegative compactly supported function has a finite translating cover by any nonzero nonnegative test function. (Haar covering ratios are finite and positive)
Open inner regularity and Borel outer regularity are required. (Radon measure on an LCH space)
Proof
Since , some real has . From and positivity at least one nonnegative part has . For choose . Positivity and invariance imply , so .
If a nonempty open had , fix . The translates cover . Any compact is covered by finitely many and hence has zero measure. Open inner regularity would give zero measure to every open set, and outer regularity would then give zero measure to every Borel set, contrary to nonzeroness. Thus every nonempty open set has positive measure.
Compact finiteness is part of the definition. A compact neighbourhood of any point contains an open neighbourhood of no larger measure, proving local finiteness. The empty set still has measure zero and the zero test function has integral zero, so neither is incorrectly included in the strict positivity assertions.
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
- Compact and discrete transforms are the two extreme Plancherel cases Corollary
- Normalized Haar probability on a compact group Corollary
- LCA Fourier inversion is not an everywhere statement for arbitrary L¹ functions Counterexample
- No normalized translation-invariant Haar probability on the real line Counterexample
- Left-uniformly continuous bounded functions (UCB) Definition
- A circle representation with an averaged orthogonal weight form Example
- Compact groups have a constant Reiter net Example
- A positive rank-one Haar average is a nonzero compact intertwiner Lemma
- A system of imprimitivity integrates to a nondegenerate representation of the transformation algebra Lemma
- A topological invariant mean yields norm-approximately invariant densities Lemma
- Averaging a Hermitian form unitarizes a finite-dimensional compact-group representation Lemma
- Central continuous approximate identities Lemma
- Characters of the L1 algebra of an abelian group Lemma
- Compact-open neighbourhoods on the dual give a neighbourhood basis on the group Lemma
- Compactly supported nonnegative transform bumps on the dual Lemma
- Compactness, finite Haar volume and invariant vectors in the regular representation Lemma
- Continuous characters separate points of an LCA group Lemma
- Finite Haar mass, compact detection, and integrable pairings Lemma
- Haar integral comparison inequality Lemma
- Haar measure on an abelian group is invariant under inversion Lemma
- L¹ of an LCA group is a commutative Banach star algebra under convolution Lemma
- LCA Fourier transforms form a dense algebra in C0 of the dual Lemma
- Local analytic separation and saturated Borel quotient images Lemma
- Matrix coefficients of finite-dimensional representations separate points of a compact group Lemma
- Nonzero multiplicative functionals on L¹ of an LCA group are Fourier evaluations Lemma
- Positive definite functions give positive bounded functionals on the transform core Lemma
- Probability-density approximation of continuous tests and topological means Lemma
- Probability-density averages and locally detectable upper essential values Lemma
- Reiter functions can be cut down to Følner sets Lemma
- Scalar unitisation of L¹ of an LCA group: characters, spectrum and identity criterion Lemma
- Smooth and K-finite vectors are dense and stable under the derived action Lemma
- Spectral measure of a unitary representation of an abelian group, covariance, and ergodicity Lemma
- Steinhaus and Pettis: Borel homomorphisms of second-countable locally compact groups are continuous Lemma
- The Bochner functional extends and has a Radon representing measure Lemma
- The Plancherel transform range is dense in L² of the dual Lemma
- Translation continuity and normalised local approximate identities on an LCA group Lemma
- Compact and locally compact abelian groups are amenable Proposition
- Compact Lie groups admit bi-invariant metrics Proposition
- The L1 group algebra has a unit exactly when the group is discrete Proposition
- Bochner's theorem for LCA groups Theorem
…and 12 more results.
Dependency tree · two levels
13 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)