LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 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.

A Reiter net has an invariant-mean cluster point

Statement

Assume the ultrafilter lemma. Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ , and let $(f_{i})_{i \in I}$ be a Reiter net on $G$ as in Reiter's condition (P1). Define $λ_{f_{i}} (φ) : = \int_{G} f_{i} φ d μ (φ \in L^{\infty} (G)) .$ Then $(λ_{f_{i}})$ has a weak-star cluster point $m$ in $L^{\infty} (G)^{*}$ . Every such cluster point is a left-invariant mean on $L^{\infty} (G)$ , so Reiter's condition (P1) implies that $G$ is amenable (Amenable locally compact group).

Facts & Assumptions

Given: The ultrafilter lemma, a locally compact Hausdorff group $G$ with fixed left Haar measure $μ$ , and a net $(f_{i})$ in the probability densities $P$ satisfying Reiter's compact-uniform translation condition.

[A1]

The ultrafilter lemma is assumed exactly as stated; Banach–Alaoglu and the compactness-to-net-cluster-point implication use this principle (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, Banach–Alaoglu, Assuming the ultrafilter lemma, compactness is equivalent to every net having a cluster point, every net having a convergent subnet, every filter having a cluster point, and every ultrafilter converging).

[F1]

$L^{\infty} (G)$ is a complex normed space of almost-everywhere classes with the essential-supremum norm; its dual consists of bounded complex-linear functionals, and weak-star convergence is pointwise convergence on $L^{\infty} (G)$ (Complex $L^{\infty}$ space of a locally compact group, The dual space X^* of a normed space and its dual norm, The weak-star topology from finite evaluations).

[F2]

For $f \in P$ , $f \geq 0$ and $\int_{G} f d μ = ∥ f ∥_{1} = 1$ ; for every $φ \in L^{\infty} (G)$ and $η > 0$ , $∣ φ ∣ \leq ∥ φ ∥_{\infty} + η$ almost everywhere. The integral is complex-linear, monotone on nonnegative functions, and satisfies the integral triangle inequality (Reiter's condition (P1), Complex Haar L^p spaces and compactly supported functions, Complex $L^{\infty}$ space of a locally compact group, Integrable real and complex functions, and their integrals, The Lebesgue integral is linear on $L^{1} (μ)$ , The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F3]

Left translations preserve Haar measure, so the substitution $x = g y$ in a Haar integral is valid; the Reiter net satisfies $∥ L_{h} f_{i} - f_{i} ∥_{1} \to 0$ for every fixed $h \in G$ (Left Haar integral and left Haar measure, Measure-preserving transformations and systems, Integral invariance under measure-preserving maps, Reiter's condition (P1)).

[F4]

The closed dual unit ball of a normed space is weak-star compact under the ultrafilter lemma. In a compact space every net has a cluster point, and each cluster point of a net is the limit of a subnet (Banach–Alaoglu, Assuming the ultrafilter lemma, compactness is equivalent to every net having a cluster point, every net having a convergent subnet, every filter having a cluster point, and every ultrafilter converging, A point is a cluster point of a net if and only if some subnet converges to it).

[F5]

A mean on $L^{\infty} (G)$ is a positive complex-linear functional with $m (1_{G}) = 1$ , and it is left-invariant when $m (L_{g} φ) = m (φ)$ for every $g$ and $φ$ (Left-invariant means on $L^{\infty}$ of a locally compact group).

[F6]

Amenability of $G$ means that such a left-invariant mean exists (Amenable locally compact group).

Proof

technique · direct

1.1F1F2

For each $i$ , define $λ_{f_{i}} (φ) = \int_{G} f_{i} φ d μ$ on $L^{\infty} (G)$ . This is independent of representatives because changing either factor on a null set changes the product only almost everywhere. For each $η > 0$ , [F2] and positivity of $f_{i}$ give $∣ f_{i} φ ∣ \leq f_{i} ∣ φ ∣ \leq f_{i} (∥ φ ∥_{\infty} + η)$ almost everywhere, so $f_{i} φ$ is integrable and $∣ λ_{f_{i}} (φ) ∣ \leq \int_{G} f_{i} ∣ φ ∣ d μ \leq (∥ φ ∥_{\infty} + η) ∥ f_{i} ∥_{1} = ∥ φ ∥_{\infty} + η$ . Letting $η ↓ 0$ proves boundedness with norm at most one. Linearity of the integral makes $λ_{f_{i}}$ complex-linear, so it lies in the closed dual unit ball of $L^{\infty} (G)^{*}$ .

1.2A1F1F2F4F5

By [A1] and [F4], the dual unit ball is weak-star compact and the net $(λ_{f_{i}})$ has a weak-star cluster point. Fix any cluster point $m$ ; [F4] supplies a subnet $(λ_{f_{i_{j}}})$ converging weak-star to $m$ . For each $φ \geq 0$ , every $λ_{f_{i_{j}}} (φ) = \int f_{i_{j}} φ d μ$ is nonnegative, so continuity of evaluation in the weak-star topology gives $m (φ) \geq 0$ . Also $λ_{f_{i_{j}}} (1_{G}) = \int f_{i_{j}} d μ = 1$ for every $j$ , hence $m (1_{G}) = 1$ . Since $m \in L^{\infty} (G)^{*}$ already, it is a mean by [F5].

2.1F1F3F5step 1.2

Fix $g \in G$ and $φ \in L^{\infty} (G)$ . Left invariance of Haar measure, with $x = g y$ , gives $λ_{f_{i}} (L_{g} φ) = \int_{G} f_{i} (x) φ (g^{- 1} x) d μ (x) = \int_{G} f_{i} (g y) φ (y) d μ (y) = λ_{L_{g^{- 1}} f_{i}} (φ)$ . Therefore $∣ λ_{f_{i}} (L_{g} φ) - λ_{f_{i}} (φ) ∣ \leq ∥ L_{g^{- 1}} f_{i} - f_{i} ∥_{1} ∥ φ ∥_{\infty} \to 0$ by [F2, F3] and the Reiter condition on the compact singleton ${g^{- 1}}$ . Along the subnet from step 1.2, weak-star convergence makes the left difference converge to $∣ m (L_{g} φ) - m (φ) ∣$ , which must consequently be zero. As $g$ and $φ$ were arbitrary, $m$ is left-invariant by [F5].

3.1F2F6step 1.2step 2.1∎

Steps 1.2 and 2.1 prove that the net has a cluster point and every cluster point is a left-invariant mean. If $G$ satisfies Reiter's condition, its equivalent net formulation [F2] supplies such a Reiter net; the cluster-point mean then witnesses amenability by [F6].

Sources

BHV, Kazhdan's Property (T), Appendix G, Theorem G.3.1, implication (iv) to (v), states that a weak-star limit point of Reiter densities is invariant. Thomas, Lecture 19, slides 5–7, records the $L^{1}$ -to-dual pairing by integration. Daws–Runde, Introduction, printed p. 1 after equation (1), explicitly states that each weak-star accumulation point of an asymptotically invariant $L^{1}$ -probability net is a left-invariant mean. The present proof supplies the complex-functional well-definedness, the exact Haar substitution, and the ultrafilter-lemma assumption at the dual-ball compactness step.

Depends on

Used by

Dependency tree · two levels

73 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

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (standard reference, not scraped)
Anne Thomas, The Banach-Tarski Paradox and Amenability, Lecture 19: Reiter's Property and the Folner Condition (standard reference, not scraped)
Matthew Daws and Volker Runde, Reiter's properties (P1) and (P2) for locally compact quantum groups, arXiv:0705.3432v5 (standard reference, not scraped)