LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

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.

Finite Haar mass, compact detection, and integrable pairings

Statement

Assume AC (The Axiom of Choice). Let $G$ be an arbitrary locally compact Hausdorff group with its fixed left Haar measure $μ$ under Left Haar integral and left Haar measure, and let $A \subseteq G$ be Borel. The following are equivalent:

$A$ contains a Borel $B$ with $0 < μ (B) < \infty$ .
Some compact $K \subseteq G$ has $μ (A \cap K) > 0$ .
Some nonnegative $f \in L^{1} (G)$ has $\int_{A} f d μ > 0$ .

Call $A$ locally null when $μ (A \cap K) = 0$ for every compact $K$ . Thus a locally null Borel set is annihilated by every $L^{1}$ pairing, even though it need not be globally $μ$ -null. Positive global Haar measure alone does not imply these equivalent conditions; the counterexample in Remarks retains the original scaffold's obstruction. No sigma-compactness, semifiniteness or locally-null quotient convention is assumed.

Facts & Assumptions

Given: AC; an LCH group $G$ with fixed Haar measure $μ$ ; and a Borel set $A$ .

[F1]

Haar measure is outer regular on Borel sets, inner regular on opens and finite on compact sets (Left Haar integral and left Haar measure, Radon measure on an LCH space).

[F2]

Nonnegative $L^{1}$ classes have Borel representatives and finite integral; indicators have integral equal to the measure, and integrals are monotone and positively homogeneous (Complex Haar L^p spaces and compactly supported functions, Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions).

[F3]

Countable unions of measurable null sets are null by countable subadditivity; a nonnegative measurable function has zero integral exactly when it is zero almost everywhere (Finite and countable subadditivity of measures, A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

[F4]

Compact subsets of a Hausdorff space are closed, hence Borel (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, The Borel sigma-algebra of a topological space).

Proof

technique · detect positive finite mass by compact intersections and by integrable threshold sets

1.1F1F4choosealgebra

Suppose (1), and put $b = μ (B) > 0$ . By [F1] choose open $O \supseteq B$ with $μ (O) < 5 b / 4 < \infty$ , then compact $K \subseteq O$ with $μ (K) > μ (O) - b / 4$ . Finite additivity inside the finite-measure $O$ gives $μ (O ∖ K) < b / 4$ , and therefore $μ (B \cap K) \geq b - μ (O ∖ K) > 0$ . Since $B \subseteq A$ , this proves (2). Conversely, under (2), $B = A \cap K$ is Borel by [F4] and has positive measure at most $μ (K) < \infty$ , proving (1). This argument uses compact inner approximation only for the open finite-measure set $O$ .

2.1F2F3step 1.1constructalgebra∎

Under (1), $f = 1_{B}$ is nonnegative in $L^{1}$ and $\int_{A} f = μ (B) > 0$ , so (3) holds. Conversely, suppose (3) and take a nonnegative finite-valued Borel representative of $f$ , modifying a null set if necessary. For $n \geq 0$ , each $E_{n} = A \cap {f > 1 / (n + 1)}$ is Borel with $μ (E_{n}) \leq (n + 1) \int_{G} f < \infty$ by [F2]. If every $E_{n}$ were null, their union $A \cap {f > 0}$ would be null by [F3], implying $\int_{A} f = 0$ , a contradiction. Thus some $E_{n}$ has positive finite measure and proves (1). The equivalence also proves that every locally null Borel $A$ has $\int_{A} f = 0$ for all nonnegative $f \in L^{1}$ ; applying this to $∣ u ∣$ gives annihilation of every complex $L^{1}$ pairing.

Remarks

The original claim that every globally positive Borel set contains a finite-positive subset is false under the actual Haar convention. Under AC let $D = R$ be discrete, $G = T \times D$ , and $A = {1} \times D$ . The compact open slices have common Haar measure $c > 0$ and normalized torus measure $c λ$ . Every compact set meets finitely many slices. For countable $S \subseteq D$ , arcs around $1$ in its slices can have total measure below any prescribed positive number; open inner regularity and outer regularity give $μ ({1} \times S) = 0$ . For uncountable $S$ , every open cover has positive arc measure in each slice. Some positive reciprocal threshold is exceeded on uncountably many slices; arbitrarily large finite unions of compact subsets of those slices force the open cover to have infinite measure, and outer regularity gives $μ ({1} \times S) = \infty$ . Every subset of $A$ is Borel because it is ${1} \times S$ with $S$ clopen in $D$ . Thus $A$ is locally null and globally infinite, with no finite-positive Borel subset. This explicit obstruction is retained; the repaired equivalence gives its precise finite-detectability domain instead of changing the measure convention.

Depends on

Used by

Dependency tree · two levels

143 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

Donald L. Cohn, Measure Theory, 2nd ed., §7.2 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 (standard reference, not scraped)
Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press, 2008; author-hosted complete text) (standard reference, not scraped)
Nicolas Bourbaki, Integration I (Chapters 1–6), Chapter V and Historical Notes on Haar measure (standard reference, not scraped)
Anne Thomas, The Banach-Tarski Paradox and Amenability, Lecture 20: Invariant Mean implies Reiter's Property (University of Sydney Honours lecture notes, 11 October 2012) (standard reference, not scraped)