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.

Følner nets give Reiter nets

Statement

Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ , and let $F \subseteq G$ be Borel with $0 < μ (F) < \infty$ . The class $f_{F} : = μ (F)^{- 1} 1_{F} \in L^{1} (G)$ belongs to $P$ from Reiter's condition (P1), and for every $x \in G$ , $∥ L_{x} f_{F} - f_{F} ∥_{1} = \frac{μ (x F △ F)}{μ (F)} .$ Consequently, every left Følner net $(F_{i})$ gives a Reiter net $(f_{F_{i}})$ . In particular, the left Følner condition implies Reiter's condition (P1).

Facts & Assumptions

Given: A locally compact Hausdorff group $G$ with left Haar measure $μ$ and a Borel set $F$ with $0 < μ (F) < \infty$ .

[A1]

Left translation carries Borel sets to Borel sets and preserves $μ$ ; thus $μ (x F) = μ (F)$ and $μ (x F △ F) \leq 2 μ (F)$ (Left Haar integral and left Haar measure, A continuous map has Borel preimages of Borel sets).

[F1]

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

[F2]

An indicator of a Borel set is a nonnegative simple measurable function; its nonnegative Lebesgue integral is its simple integral, namely the measure of that set (A measurable function between measurable spaces, Nonnegative simple measurable functions, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions).

Proof

technique · direct

1.1F1F2givenconstructalgebra

The indicator $1_{F}$ is Borel measurable and simple. By [F2], $\int_{G} 1_{F} d μ = μ (F)$ , so the nonnegative Borel function $μ (F)^{- 1} 1_{F}$ has finite integral and defines an $L^{1} (G)$ class. It is nonnegative and $∥ f_{F} ∥_{1} = μ (F)^{- 1} \int_{G} 1_{F} d μ = 1$ ; hence $f_{F} \in P$ .

1.2A1F1F2algebra

For every $x, y \in G$ , $(L_{x} 1_{F}) (y) = 1_{F} (x^{- 1} y) = 1_{x F} (y)$ . Thus $L_{x} f_{F} - f_{F} = μ (F)^{- 1} (1_{x F} - 1_{F})$ , whose modulus is $μ (F)^{- 1} 1_{x F △ F}$ . The symmetric difference is Borel and has finite measure by [A1]. Applying [F2] to its indicator gives $∥ L_{x} f_{F} - f_{F} ∥_{1} = μ (F)^{- 1} \int_{G} 1_{x F △ F} d μ = \frac{μ (x F △ F)}{μ (F)}$ .

2.1step 1.1step 1.2givenconstruct∎

If $(F_{i})$ is a left Følner net, set $f_{i} : = f_{F_{i}}$ . Steps 1.1 and 1.2 show that $f_{i} \in P$ and, for every compact $Q$ , $Δ_{Q} (f_{i}) = Δ_{Q} (F_{i})$ , since the pointwise discrepancies agree for each $x \in Q$ . The defining eventual estimates therefore make $(f_{i})$ a Reiter net. If only the single-set left Følner condition is given, for each compact $Q$ and $ε > 0$ choose a Følner witness $F$ ; step 1.1 gives $f_{F} \in P$ and step 1.2 gives the same estimate, so Reiter's condition (P1) holds. This uses one witness at a time and no global choice function.

Depends on

Used by

The Følner criterion for locally compact groups Theorem

Dependency tree · two levels

29 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)
Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (standard reference, not scraped)