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

Reiter's condition (P1)

Definition

Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ , and put $P : = {f \in L^{1} (G) : f \geq 0, ∥ f ∥_{1} = 1},$ where $f \geq 0$ means that the class has a real-valued representative that is nonnegative almost everywhere. For $g \in G$ define $(L_{g} f) (x) : = f (g^{- 1} x)$ on almost-everywhere classes. For compact $Q \subseteq G$ and $f \in P$ , set $Δ_{Q} (f) : = \sup ({0} \cup {∥ L_{g} f - f ∥_{1} : g \in Q}) .$ Then $0 \leq Δ_{Q} (f) \leq 2$ , and $Δ_{\emptyset} (f) = 0$ . The group $G$ satisfies Reiter's condition (P1) if for every compact $Q \subseteq G$ and every $ε > 0$ there is $f \in P$ with $Δ_{Q} (f) \leq ε$ .

Equivalently, there is a net $(f_{i})_{i \in I}$ in $P$ with its inherited $L^{1}$ -norm topology such that for every compact $Q$ and every $ε > 0$ some $i_{0} \in I$ satisfies $Δ_{Q} (f_{i}) \leq ε$ for all $i ⪰ i_{0}$ ; this is uniform convergence to zero on compact subsets. The set $P$ is convex and $L_{g} P = P$ for every $g \in G$ . Only left translates are used, the measure $μ$ is fixed, and no compactness assumption on $G$ is made.

Facts & Assumptions

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

[A1]

For each $g \in G$ , the map $T_{g} (x) = g^{- 1} x$ is Borel measurable and measure-preserving: $T_{g}^{- 1} (E) = g E$ and $μ (g E) = μ (E)$ for Borel $E \subseteq G$ . Thus it induces $L_{g} f = f \circ T_{g}$ on almost-everywhere classes (Left Haar integral and left Haar measure, A continuous map has Borel preimages of Borel sets, Measure-preserving transformations and systems).

[F1]

$L^{1} (G)$ consists of complex measurable almost-everywhere classes with $∥ f ∥_{1} = \int_{G} ∣ f ∣ d μ$ ; if $f \geq 0$ , then $\int_{G} f = ∥ f ∥_{1}$ (Complex Haar L^p spaces and compactly supported functions).

[F2]

Integrals are invariant under measure-preserving maps, and the integral is complex-linear on $L^{1} (G)$ (Integral invariance under measure-preserving maps, The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F3]

A net is a function indexed by a nonempty directed preorder; antisymmetry is not required (Directed preorders and nets).

Proof

technique · direct

1.1A1F1F2algebra

If $f \in P$ , then [A1] makes $L_{g} f$ well-defined on classes and preserves nonnegativity. By [F2], $∥ L_{g} f ∥_{1} = \int_{G} ∣ f \circ T_{g} ∣ d μ = \int_{G} ∣ f ∣ d μ = 1$ . Thus $L_{g} P \subseteq P$ ; applying the same argument to $g^{- 1}$ and using $L_{g^{- 1}} L_{g} = I$ gives equality. Also, for every $g \in G$ , $∥ L_{g} f - f ∥_{1} \leq ∥ L_{g} f ∥_{1} + ∥ f ∥_{1} = 2$ , so the supremum defining $Δ_{Q} (f)$ is finite and lies in $[0, 2]$ , including the empty-test value zero.

1.2F1F2constructalgebra

For $f, h \in P$ and $t \in [0, 1]$ , choose nonnegative real representatives. Their convex combination is nonnegative and, by [F2], $∥ t f + (1 - t) h ∥_{1} = \int_{G} (t f + (1 - t) h) d μ = t ∥ f ∥_{1} + (1 - t) ∥ h ∥_{1} = 1$ . Therefore $t f + (1 - t) h \in P$ and $P$ is convex.

2.1F3step 1.1given

If $(f_{i})_{i \in I}$ is a net satisfying the compact-uniform condition, then for any compact $Q$ and $ε > 0$ its defining eventual estimate supplies $i_{0}$ with $Δ_{Q} (f_{i}) \leq ε$ for all $i ⪰ i_{0}$ . In particular $f_{i_{0}} \in P$ is a witness to Reiter's condition.

3.1F3constructalgebra∎

Conversely, assume Reiter's condition. Let $I$ be the set of all triples $(Q, ε, f)$ with $Q$ compact, $ε > 0$ , $f \in P$ , and $Δ_{Q} (f) \leq ε$ . Order them by $(Q, ε, f) ⪯ (Q^{'}, ε^{'}, f^{'})$ exactly when $Q \subseteq Q^{'}$ and $ε^{'} \leq ε$ . It is nonempty, since the condition at the compact singleton ${e}$ and $ε = 1$ supplies a witness. It is directed: for two indices apply the condition to the compact union of their test sets, which is compact as a finite union, and the positive minimum of their tolerances, obtaining a witness that gives a common upper bound. By [F3], the third-coordinate map $i \mapsto f_{i}$ is a net. Given any compact $Q$ and $ε > 0$ , the condition supplies $i_{0} = (Q, ε, f_{0})$ ; every $i ⪰ i_{0}$ then has $Δ_{Q} (f_{i}) \leq Δ_{Q_{i}} (f_{i}) \leq ε_{i} \leq ε$ . Every index carries its own witness, so no global choice function is used.

Depends on

Used by

Dependency tree · two levels

26 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)
Matthew Daws and Volker Runde, Reiter's properties (P1) and (P2) for locally compact quantum groups, arXiv:0705.3432v5 (standard reference, not scraped)