LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Counting measure on a discrete group is Haar, Haar measures there are its multiples, and integrals against them are sums

Statement

Let $G$ be an LCH group whose topology is discrete, let $#_{G}$ be the counting set function on the subsets of $G$ (Counting measure on an arbitrary set), and let $\sum_{y \in G}$ be the sum of Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ . Then:

$#_{G}$ is a left Haar measure and a right Haar measure on $G$ .
Every left Haar measure $μ$ on $G$ satisfies $μ (E) = c #_{G} (E)$ for every $E \subseteq G$ , with $c : = μ ({e}) > 0$ ; this $c$ is unique.
For every $H : G \to [0, + \infty)$ one has $\int_{G} H d μ = c \sum_{y \in G} H (y)$ , and every $μ$ -integrable complex $H$ satisfies $\int_{G} H d μ = c \sum_{y \in G} H (y)$ together with $\sum_{y \in G} ∣ H (y) ∣ < + \infty$ .

Facts & Assumptions

Given: An LCH group $G$ whose topology is discrete, and a left Haar measure $μ$ on $G$ .

[F1]

The discrete topology on $G$ is the power set $P (G)$ , so every subset of $G$ is open and closed; hence the Borel $σ$ -algebra of $G$ is $P (G)$ and every function on $G$ is Borel measurable (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, The Borel sigma-algebra of a topological space, Extended-real-valued measurable functions).

[F2]

A space is compact when every open cover has a finite subcover (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F3]

The counting set function satisfies $#_{G} (E) = ∣ E ∣$ for finite $E$ and $#_{G} (E) = + \infty$ for infinite $E$ , and it is a measure on $(G, P (G))$ ; hence it vanishes at $\emptyset$ , is additive over disjoint unions and is monotone under inclusion, and a bijection of $G$ carries a set to a set of the same counting measure (Counting measure on an arbitrary set, Counting measure is a measure, Measures on sigma-algebras).

[F4]

A left Haar measure is a nonzero Borel measure on $G$ that is left invariant, finite on compact sets, outer regular on Borel sets and inner regular on open sets; a right Haar measure is the same with right translations in place of left ones (Left Haar integral and left Haar measure, Radon measure on an LCH space).

[F5]

A nonnegative simple measurable function is a measurable finite-valued function $G \to [0, + \infty)$ with finite range; pairwise disjoint Borel sets $E_{1}, \dots, E_{m}$ with coefficients $a_{j} \geq 0$ and $s = \sum_{j = 1}^{m} a_{j} χ_{E_{j}}$ form a simple representation of $s$ , the simple integral is $\sum_{j = 1}^{m} a_{j} ν (E_{j})$ under the convention $0 \cdot (+ \infty) = 0$ , and its value is independent of the representation (Nonnegative simple measurable functions, The integral of a nonnegative simple function, The simple integral is independent of the chosen representation).

[F6]

The nonnegative Lebesgue integral of a measurable $H \geq 0$ is the supremum of the simple integrals of its nonnegative simple minorants, and equals the simple integral when $H$ itself is simple (The nonnegative Lebesgue integral, The nonnegative integral agrees with the simple integral on simple functions).

[F7]

For a nonnegative family $(d_{y})_{y \in G}$ the sum $\sum_{y \in G} d_{y}$ is the supremum of its finite subsums; a scalar family is absolutely summable when this sum of moduli is finite, absolutely summable families are summable with a $C$ -linear sum, and $∣ \sum_{y \in G} a_{y} ∣ \leq \sum_{y \in G} ∣ a_{y} ∣$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

[F8]

Finite sums over a commutative monoid are invariant under a bijective reindexing of the finite index set and split over a disjoint decomposition of that set (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F9]

A complex function $H = u + i v$ with $u = Re H$ , $v = Im H$ is $μ$ -integrable exactly when $\int_{G} ∣ H ∣ d μ < + \infty$ , and then $\int_{G} H d μ = \int_{G} u d μ + i \int_{G} v d μ$ while $\int_{G} u d μ = \int_{G} u^{+} d μ - \int_{G} u^{-} d μ$ (Integrable real and complex functions, and their integrals, Real and imaginary parts, complex conjugation, and modulus).

Proof

technique · direct

1.1

$#_{G}$ is a Borel measure: by [F1] every subset of $G$ is Borel, so $P (G)$ is the Borel $σ$ -algebra of $G$ and the measure of [F3] is defined on it.

F1F3

1.2

Invariance. For $a \in G$ the translations $x \mapsto a x$ and $x \mapsto x a$ are bijections of $G$ , with inverses $y \mapsto a^{- 1} y$ and $y \mapsto y a^{- 1}$ , so by [F3] they preserve the counting measure: $#_{G} (a E) = #_{G} (E) = #_{G} (E a)$ for every $E \subseteq G$ .

1.3

Compact subsets are finite. Let $K \subseteq G$ be compact; its singletons are open by [F1] and form an open cover of $K$ , so [F2] provides finitely many of them that cover $K$ , and $K$ is finite.

F1F2

1.4

Equal mass of singletons. Put $d : = μ ({e})$ . For $x \in G$ left invariance and finite additivity give $μ ({x}) = μ (x {e}) = μ ({e}) = d$ , and for finite $F \subseteq G$ therefore $μ (F) = \sum_{x \in F} μ ({x}) = ∣ F ∣ d$ .

F3F4given

2.1

Compact finiteness and regularity of $#_{G}$ . A compact $K$ is finite by step 1.3, so $#_{G} (K) = ∣ K ∣ < + \infty$ by [F3]; every subset $E$ is open by [F1] and is an admissible open superset of itself, so monotonicity in [F3] makes the infimum in the outer regularity condition equal to $#_{G} (E)$ ; and for open $U$ , step 1.3 makes the compact subsets of $U$ exactly its finite subsets, with $\sup {∣ F ∣ : F \subseteq U finite} = #_{G} (U)$ , since that supremum is $∣ U ∣$ when $U$ is finite, attained at $F = U$ , and $+ \infty$ when $U$ is infinite, an infinite set containing a subset of each finite cardinality by induction on the size (a set containing a subset of $n$ elements and being infinite has a further element).

F1F3step 1.3

2.2

$d > 0$ . If $d = 0$ , then step 1.4 gives $μ (F) = 0$ for every finite $F$ ; compact sets are finite by step 1.3, so inner regularity [F4] gives $μ (U) = \sup {μ (K) : K \subseteq U compact} = 0$ for every open $U$ ; since every subset is open by [F1], $μ$ would vanish identically, contradicting its nonzeroness in [F4].

F1F4step 1.3step 1.4

3.1

Clause 1. $#_{G} ({e}) = 1$ , so $#_{G}$ is nonzero, and step 1.1, step 1.2 and step 2.1 verify every requirement of a left Haar measure listed in [F4]; the same invariance gives right invariance, so $#_{G}$ is a right Haar measure as well.

F3F4step 1.1step 1.2step 2.1

3.2

Clause 2. For every $E \subseteq G$ the set $E$ is open by [F1], so inner regularity [F4] with step 1.3, step 1.4 and step 2.1 gives $μ (E) = \sup {μ (K) : K \subseteq E compact} = \sup {∣ K ∣ d : K \subseteq E finite} = d \cdot #_{G} (E)$ , the last equality by the computation of step 2.1 and by $d > 0$ from step 2.2, which lets $d$ be pulled out of the supremum, both sides being $+ \infty$ for infinite $E$ ; and if also $μ = c^{'} #_{G}$ with $c^{'} > 0$ , then evaluation at ${e}$ gives $c^{'} = c^{'} #_{G} ({e}) = μ ({e}) = d$ , so the constant $c = d$ is unique.

F1F3F4step 1.3step 1.4step 2.1step 2.2

3.3

Finite sums of a simple function. Let $s = \sum_{j = 1}^{m} a_{j} χ_{E_{j}}$ be a simple representation and let $F \subseteq G$ be finite. Pairwise disjointness gives $s (y) = \sum_{j : y \in E_{j}} a_{j}$ for $y \in F$ , so [F8] yields $\sum_{y \in F} s (y) = \sum_{j = 1}^{m} a_{j} ∣ E_{j} \cap F ∣$ , which is at most $\sum_{j = 1}^{m} a_{j} #_{G} (E_{j})$ by [F3]; conversely, choosing for each $j$ a finite subset of $E_{j}$ of size $\min (n, #_{G} (E_{j}))$ , possible by the induction in step 2.1, gives a finite $F$ with $\sum_{y \in F} s (y) = \sum_{j = 1}^{m} a_{j} \min (n, #_{G} (E_{j}))$ , whose supremum over $n$ is $\sum_{j = 1}^{m} a_{j} #_{G} (E_{j})$ . Hence $\sum_{y \in G} s (y) = \sum_{j = 1}^{m} a_{j} #_{G} (E_{j})$ .

F3F7F8step 2.1

4.1

Lower bound. Let $H : G \to [0, + \infty)$ and let $F \subseteq G$ be finite. The function $H χ_{F} = \sum_{y \in F} H (y) χ_{{y}}$ is nonnegative simple, because it is finite-valued with finite range and the singletons are Borel by [F1]; its simple integral against $μ$ is $\sum_{y \in F} H (y) μ ({y}) = c \sum_{y \in F} H (y)$ by [F5] and step 3.2. Since $H χ_{F} \leq H$ , [F6] gives $\int_{G} H d μ \geq c \sum_{y \in F} H (y)$ for every finite $F$ , and the supremum over $F$ with [F7] gives $\int_{G} H d μ \geq c \sum_{y \in G} H (y)$ .

F1F5F6F7step 3.2

4.2

Upper bound. Let $s \leq H$ be a nonnegative simple minorant. By [F5], step 3.2 and step 3.3 its simple integral is $\sum_{j = 1}^{m} a_{j} μ (E_{j}) = \sum_{j = 1}^{m} a_{j} c #_{G} (E_{j}) = c \sum_{j = 1}^{m} a_{j} #_{G} (E_{j}) = c \sum_{y \in G} s (y)$ , finite sums of nonnegative extended reals being rescaled by the positive constant $c$ ; and $\sum_{y \in G} s (y) \leq \sum_{y \in G} H (y)$ , because $s \leq H$ compares all finite subsums termwise. So every simple minorant of $H$ has simple integral at most $c \sum_{y \in G} H (y)$ , and [F6] gives $\int_{G} H d μ \leq c \sum_{y \in G} H (y)$ .

F5F6F7step 3.2step 3.3

5.1

Clause 3, first half. Step 4.1 and step 4.2 give $\int_{G} H d μ = c \sum_{y \in G} H (y)$ for every $H : G \to [0, + \infty)$ .

step 4.1step 4.2

6.1

Clause 3, second half, and conclusion. Let $H = u + i v$ be $μ$ -integrable. Then $∣ H ∣$ is finite-valued nonnegative with $\int_{G} ∣ H ∣ d μ < + \infty$ by [F9], so step 5.1 gives $\sum_{y \in G} ∣ H (y) ∣ = c^{- 1} \int_{G} ∣ H ∣ d μ < + \infty$ and hence absolute summability of $(H (y))_{y \in G}$ by [F7]; the four functions $u^{+}, u^{-}, v^{+}, v^{-}$ are finite-valued nonnegative with sums bounded by $\sum_{y \in G} ∣ H (y) ∣$ , so they are summable as well, and [F7] with $H = u^{+} - u^{-} + i (v^{+} - v^{-})$ gives $\sum_{y \in G} H (y) = \sum_{y \in G} u^{+} - \sum_{y \in G} u^{-} + i (\sum_{y \in G} v^{+} - \sum_{y \in G} v^{-})$ . Using [F9] for the integral and step 5.1 for each of the four parts, $\int_{G} H d μ = (\int_{G} u^{+} d μ - \int_{G} u^{-} d μ) + i (\int_{G} v^{+} d μ - \int_{G} v^{-} d μ) = c (\sum_{y \in G} u^{+} - \sum_{y \in G} u^{-} + i (\sum_{y \in G} v^{+} - \sum_{y \in G} v^{-})) = c \sum_{y \in G} H (y)$ , the second half of clause 3, which completes the proof. ∎

F7F9step 5.1

Remarks

Choice cost. The argument is choice-free. The compactness-to-finiteness step uses the finite subcover of one explicitly given cover, the subsets of prescribed finite size are produced by induction rather than by selection, and the suprema are taken in $[0, + \infty]$ . In particular the general uniqueness theorem for Haar measures, which assumes AC, is not used here: on a discrete group the proportionality constant is pinned to $μ ({e})$ .
Finite-valued integrands. Clause 3 is stated for $H : G \to [0, + \infty)$ , which covers every integrand used on this page; the value $+ \infty$ is excluded because the simple minorants in step 4.1 and step 4.2 would then need the truncation convention of the extended nonnegative integral.
Reading the clauses. Clause 2 identifies a left Haar measure on a discrete group as $c \cdot counting$ with $c = μ ({e})$ , and clause 3 turns integrals against it into the corresponding absolutely convergent sums; both are used by the discrete cases of the unimodularity and convolution items on this page.

Depends on

Used by

Convolution on a discrete group Example
Compact, discrete and abelian groups are unimodular Proposition
The L1 group algebra has a unit exactly when the group is discrete Proposition

Dependency tree · two levels

60 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

Lynn Loomis, An Introduction to Abstract Harmonic Analysis, §§30–31 (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis, VI §2 (standard reference, not scraped)