TheoremStatement: 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.

The Følner criterion for locally compact groups

Statement

Assume AC. Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ . Then $G$ is amenable (Amenable locally compact group) if and only if it satisfies the left Følner condition (Left Følner nets for locally compact groups): for every compact $Q \subseteq G$ and every $ε > 0$ there is a Borel set $F \subseteq G$ with $0 < μ (F) < \infty$ and $Δ_{Q} (F) \leq ε$ . Equivalently, $G$ admits a left Følner net. Borel sets suffice for $F$ .

Facts & Assumptions

Given: AC, a locally compact Hausdorff group $G$ , and a fixed left Haar measure $μ$ .

[A1]

AC is the choice-function principle (The Axiom of Choice). It implies AC $ω$ : for any sequence $(X_{n})$ of nonempty sets, apply AC to the range family ${X_{n} : n \in N}$ and use the resulting selector at each $X_{n}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

Amenability is equivalent to Reiter's condition (P1) for locally compact Hausdorff groups under AC; (P1) means compact-uniform approximate invariance of nonnegative norm-one $L^{1}$ functions (Amenability is equivalent to Reiter's condition (P1), Reiter's condition (P1)).

[F2]

For nonnegative $f \in L^{1} (G)$ , its superlevel sets $E_{t} = {y : f (y) \geq t}$ satisfy $\int_{0}^{\infty} μ (E_{t}) d t = ∥ f ∥_{1}$ and $\int_{0}^{\infty} μ (E_{t} △ E_{t}^{'}) d t = ∥ f - g ∥_{1}$ for any nonnegative $g \in L^{1} (G)$ with corresponding superlevel sets $E_{t}^{'}$ ; no global $σ$ -finiteness of Haar measure is required (The layer-cake identity for integrable functions).

[F3]

If $f \geq 0$ and $∥ f ∥_{1} = 1$ , then $μ ({f \geq t}) \leq 1 / t$ for every $t > 0$ (Chebyshev-Markov inequality for the integral).

[F4]

Left Haar measure is left invariant, finite on compact sets, and positive on nonempty open sets (Left Haar integral and left Haar measure, Haar measure is positive on nonempty open sets and finite on compact sets).

[F5]

Under AC, $x \mapsto L_{x} u$ is norm-continuous in $L^{1} (G)$ for each $u \in L^{1} (G)$ , and every $L_{x}$ is an isometry (Strong continuity of left and modular right translations on L1 and L2).

[F6]

Every identity in a locally compact Hausdorff group has a compact neighbourhood; finite products of compact spaces are compact, and continuous images of compact spaces are compact (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, A product of finitely many compact spaces is compact in the product topology, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, Topological group: multiplication and inversion are continuous).

[F7]

Tonelli interchanges nonnegative integrals on a product of $σ$ -finite measure spaces, and pointwise limits of measurable real functions are measurable (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable).

[F8]

For a Borel set $F$ with $0 < μ (F) < \infty$ , the normalized indicator $μ (F)^{- 1} 1_{F}$ is a Reiter probability density with translation defect exactly $μ (x F △ F) / μ (F)$ (Følner nets give Reiter nets).

[F9]

A net of positive finite-measure Borel sets satisfies the left Følner condition exactly when the single-set condition in the Statement holds (Left Følner nets for locally compact groups).

[F10]

A compact subset of a Hausdorff space is closed, hence Borel (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, 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).

[F11]

$L^{1} (G)$ is formed from measurable functions for the fixed Borel Haar measure; every class therefore has a Borel representative, and replacing a representative by its positive part preserves its class when the class is nonnegative (Complex Haar L^p spaces and compactly supported functions, Left Haar integral and left Haar measure, The Borel sigma-algebra of a topological space).

[F12]

Amenability of $G$ means existence of a left-invariant mean on $L^{\infty} (G)$ (Amenable locally compact group).

Proof

Given: AC and a locally compact Hausdorff group $G$ with fixed left Haar measure $μ$ .

Proof technique: direct.

1.1F1F12given

Suppose $G$ is amenable in the sense of [F12]. By [F1], $G$ satisfies Reiter's condition (P1).

1.2F1F4F6F10givenconstruct

Assume (P1), fix a compact target $Q \subseteq G$ and $ε > 0$ , and put $η : = ε / 2$ . Choose a compact neighbourhood $C$ of the identity and an open identity neighbourhood $O \subseteq C$ . Set $P : = Q \cup C$ and $K : = P^{2}$ . Then $P$ is compact, contains the identity, and $0 < μ (P) < \infty$ because $O \subseteq P$ and [F4]; $K$ is compact and Borel by [F6] and [F10], and $0 < μ (K) < \infty$ because $P \subseteq K$ . Choose $f \in L^{1} (G)$ with $f \geq 0$ , $∥ f ∥_{1} = 1$ and $\sup_{x \in K} ∥ L_{x} f - f ∥_{1} \leq η μ (P) / (4 μ (K))$ , using (P1) with this positive tolerance.

1.3F1F8F9F12

Conversely, suppose $G$ satisfies the left Følner condition. By [F8], normalized indicators of its Følner witnesses give (P1) (equivalently use a Følner net by [F9]); [F1] then implies that $G$ is amenable in the sense of [F12].

2.1A1F2F3F4F5F7F8F11step 1.2algebra

By [F11] choose a nonnegative Borel representative of $f$ and set $E_{t} : = {y : f (y) \geq t}$ for $t > 0$ . By [F2] and [F3], $\int_{0}^{\infty} μ (E_{t}) d t = 1$ and $μ (E_{t}) < \infty$ for every $t > 0$ . For each $t$ with $μ (E_{t}) > 0$ , [F8] applied to $E_{t}$ gives $μ (x E_{t} △ E_{t}) = ∥ L_{x} 1_{E_{t}} - 1_{E_{t}} ∥_{1}$ ; when $μ (E_{t}) = 0$ , both sides vanish by [F4]. Thus the boundary function is continuous in $x$ by [F5]. Put $D (x, t) : = ∥ L_{x} 1_{E_{t}} - 1_{E_{t}} ∥_{1}$ . On each level interval $[1 / n, n]$ , for all sufficiently large $m$ put $t_{m} (t) : = 2^{- m} ⌊ 2^{m} t ⌋ > 0$ . Then $t_{m} (t) ↑ t$ , so the finite-measure sets $E_{t_{m} (t)}$ decrease to $E_{t}$ and $∥ 1_{E_{t_{m} (t)}} - 1_{E_{t}} ∥_{1} \to 0$ by countable additivity. For fixed $m$ , $D (x, t_{m} (t))$ is product-measurable: it has countably many Borel level-parameter cells, and on each cell is a continuous function of $x$ by [F5]. Isometry gives $∣ D (x, t_{m} (t)) - D (x, t) ∣ \leq 2 ∥ 1_{E_{t_{m} (t)}} - 1_{E_{t}} ∥_{1}$ , so taking the pointwise limit proves product measurability on $K \times [1 / n, n]$ . These intervals cover $(0, \infty)$ , proving the needed product measurability without second countability. Since Haar measure restricted to $K$ is finite and the level parameter has $σ$ -finite Lebesgue measure, [F7] and [F2] give $\int_{0}^{\infty} μ (E_{t}) r (t) d t = \int_{K} ∥ L_{x} f - f ∥_{1} d μ (x) \leq η μ (P) / 4$ , where $r (t) : = \int_{K} μ (x E_{t} △ E_{t}) / μ (E_{t}) d μ (x)$ when $μ (E_{t}) > 0$ , and $r (t) : = 0$ otherwise. Since $\int_{0}^{\infty} μ (E_{t}) d t = 1$ , some $t > 0$ has $0 < μ (E_{t}) < \infty$ and $r (t) < η μ (P) / 2$ .

3.1F3F4F5F10step 2.1algebra

Fix such a $t$ and put $A : = {x \in K : μ (x E_{t} △ E_{t}) / μ (E_{t}) \leq η}$ . The boundary function is continuous, so $A$ is Borel; Markov's inequality gives $μ (K ∖ A) \leq r (t) / η < μ (P) / 2$ . For any $x \in P$ , $x P \subseteq x K \cap K$ because $P \subseteq K$ and $P^{2} = K$ , so $μ (x K \cap K) \geq μ (x P) = μ (P)$ . Also $x K \cap K \subseteq (x A \cap A) \cup x (K ∖ A) \cup (K ∖ A)$ , hence $μ (x A \cap A) > 0$ . Therefore there exist $a_{1}, a_{2} \in A$ with $x = a_{1} a_{2}^{- 1}$ . By left invariance and the triangle inequality for symmetric difference, $μ (x E_{t} △ E_{t}) \leq μ (a_{2}^{- 1} E_{t} △ E_{t}) + μ (a_{1} E_{t} △ E_{t}) = μ (a_{2} E_{t} △ E_{t}) + μ (a_{1} E_{t} △ E_{t}) \leq 2 η μ (E_{t}) = ε μ (E_{t})$ . Thus $F : = E_{t}$ is Borel with positive finite measure and satisfies the required estimate for every $x \in P$ , hence $Δ_{Q} (F) \leq ε$ .

4.1A1F1F2F5F9F12step 1.1step 1.2step 1.3step 2.1step 3.1∎

Steps 1.1, 1.2, 2.1, and 3.1 prove amenability implies the Følner condition; step 1.3 proves the reverse implication. Step 3.1 produces Borel witnesses even when the condition is initially phrased with measurable sets, and [F9] gives the equivalent net formulation. The only Choice assumption is the stated AC, used through [F1], [F5], and AC $ω$ for [F2].

Sources

BHV, Kazhdan's Property (T), Appendix G.5, Theorem G.5.1 and its proof, states the Følner criterion and gives the complete Reiter-to-Følner level-set extraction for a compact test set containing the identity. The proof here enlarges every target compact set to a compact identity neighbourhood, ensuring the positive finite Haar measure required in the averaging estimates, and justifies the compact-parameter Tonelli step under arbitrary LCH generality. Thomas, Lecture 19, slides 14–18, gives the same extraction route.

Depends on

Used by

Folner sequences for second countable compactly generated groups Corollary
Følner sets in ℝⁿ Example

Dependency tree · two levels

114 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 Følner Condition (standard reference, not scraped)