LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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 functions can be cut down to Følner sets

Statement

Assume AC. Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ , let $Q \subseteq G$ be compact with $μ (Q) > 0$ , let $ε > 0$ , and let $f \in L^{1} (G)$ satisfy $f \geq 0$ , $∥ f ∥_{1} = 1$ and $\sup_{x \in Q^{2}} ∥ L_{x} f - f ∥_{1} \leq \frac{ε μ (Q)}{2 μ (Q^{2})},$ where $Q^{2} : = {x y : x, y \in Q}$ . Then there is a Borel set $U \subseteq G$ with $0 < μ (U) < \infty$ and $\sup_{x \in Q} \frac{μ (x U △ U)}{μ (U)} \leq 2 ε .$ Consequently Reiter's condition (P1) implies the left Følner condition: for every compact $Q$ and every $ε > 0$ a Borel set $U$ with $0 < μ (U) < \infty$ and $\sup_{x \in Q} \frac{μ (x U △ U)}{μ (U)} \leq 2 ε$ exists. The supremum over an empty compact test set in the consequent is taken to be $0$ .

Facts & Assumptions

Given: AC; an LCH group $G$ with fixed left Haar measure $μ$ ; a compact $Q$ with $μ (Q) > 0$ ; $ε > 0$ ; and a nonnegative norm-one $f \in L^{1} (G)$ satisfying the Statement's $Q^{2}$ estimate.

[F1]

Left translations $L_{a}$ are linear isometries on $L^{1} (G)$ , satisfy $L_{a} L_{b} = L_{a b}$ and have norm-continuous vector orbits under AC (Strong continuity of left and modular right translations on L1 and L2).

[F2]

Under AC, complex $L^{1} (G)$ is complete. Integrals are linear, obey the integral triangle inequality and are monotone on nonnegative functions; a nonnegative function has zero integral exactly when it is zero a.e. (Completeness of the complex Haar L1 and L2 spaces and density of Cc, The Lebesgue integral is linear on $L^{1} (μ)$ , The modulus of an integral is bounded by the integral of the modulus, A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere, Complex Haar L^p spaces and compactly supported functions).

[F3]

Left Haar measure is left invariant, finite on compact sets and positive on nonempty opens; every identity has a compact neighborhood. Finite products and continuous images preserve compactness (Left Haar integral and left Haar measure, Haar measure is positive on nonempty open sets and finite on compact sets, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Topological group: multiplication and inversion are continuous, 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).

[F4]

Under Countable Choice, layer cake gives $\int_{0}^{\infty} μ ({u \geq t}) d t = ∥ u ∥_{1}$ and the analogous symmetric-difference identity for two nonnegative integrable functions, without global sigma-finiteness. The same proof with intervals $(0, u)$ instead of $(0, u]$ gives the strict-superlevel version; their endpoints have zero Lebesgue length (The layer-cake identity for integrable functions).

[F5]

Chebyshev bounds $μ ({u > t}) \leq ∥ u ∥_{1} / t$ for $u \geq 0$ , $t > 0$ . Tonelli interchanges nonnegative product-measurable integrals on sigma-finite spaces, and pointwise limits of measurable functions are measurable (Chebyshev-Markov inequality for the integral, 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).

[F6]

Compact subsets of a Hausdorff space are closed, hence Borel, and a finite open cover can be disjointified into Borel cells by finite differences. Compactness gives finite subcovers (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, 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).

[F7]

Reiter (P1) supplies a probability density for every compact test and positive tolerance; the left Følner condition uses finite-positive Borel sets and compact-uniform boundary defects (Reiter's condition (P1), Left Følner nets for locally compact groups).

[A1]

AC implies Countable Choice by the declared implication, supplying the hypothesis in [F4]; AC also chooses the finite-partition data for each positive integer below (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · parity-average the supplied density, then combine scalar left-Haar averaging with measurable coarea to select a single uniform Følner level set

1.1F1F2F3F6A1givenconstructalgebra

Put $K = Q^{2}$ , $q = μ (Q)$ and $k = μ (K)$ . By [F3, F6], $K$ is compact Borel, $k < \infty$ , and for any $c \in Q$ , $c Q \subseteq K$ gives $k \geq q > 0$ . Let $δ = \sup_{b \in K} ∥ L_{b} f - f ∥_{1}$ , which is finite by the bound $2 ∥ f ∥_{1} = 2$ , and satisfies $δ \leq ε q / (2 k)$ . Construct the compact-orbit probability average directly in $L^{1}$ : for each $n$ , cover the compact orbit by norm balls of radius $1 / (2 n)$ , pull them back to a finite open cover of $Q$ , and disjointify by [F6]. Choose a sample from each nonempty cell; this gives a finite Borel partition $Q = ⨆_{j} E_{n, j}$ with samples $y_{n, j} \in E_{n, j}$ such that $∥ L_{y} f - L_{y_{n, j}} f ∥_{1} < 1 / n$ on each nonempty cell. Set $S_{n} = \sum_{j} μ (E_{n, j}) L_{y_{n, j}} f / q$ . Intersecting the partitions for $n, m$ and comparing their samples through a point of each nonempty intersection gives $∥ S_{n} - S_{m} ∥_{1} \leq 1 / n + 1 / m$ . Completeness in [F2] gives a limit $g$ . Every $S_{n}$ is a nonnegative probability density; convergence makes the imaginary part and negative real part of $g$ have zero $L^{1}$ norm, hence $g \geq 0$ , and norm continuity gives $∥ g ∥_{1} = 1$ . This compact finite-partition mean requires no pointwise formula for extended convolution.

2.1F1F2step 1.1constructalgebra

For each $b \in Q$ , $b y_{n, j} \in K$ , so $∥ L_{b} S_{n} - f ∥_{1} \leq δ$ and passage to the norm limit gives $∥ L_{b} g - f ∥_{1} \leq δ$ . For $a \in Q$ , fix any $c \in Q$ ; [F1] gives $∥ L_{a} f - g ∥_{1} = ∥ L_{c} L_{a} f - L_{c} g ∥_{1} \leq ∥ L_{c a} f - f ∥_{1} + ∥ f - L_{c} g ∥_{1} \leq 2 δ$ . Thus $h = (f + g) / 2$ is a probability density with $∥ L_{a} h - h ∥_{1} \leq 3 δ / 2$ for $a \in Q$ . For $x = a b \in K$ , $∥ L_{x} g - g ∥_{1} \leq ∥ L_{a} (L_{b} g - f) ∥_{1} + ∥ L_{a} f - g ∥_{1} \leq 3 δ$ ; together with $∥ L_{x} f - f ∥_{1} \leq δ$ , this gives $∥ L_{x} h - h ∥_{1} \leq 2 δ$ on $K$ . No factors were commuted.

2.2F1F2F3step 1.1algebra

For any finite-positive Borel $U$ , write $d_{a} (U) = μ (a U △ U) = ∥ L_{a} 1_{U} - 1_{U} ∥_{1}$ and $C_{P} (U) = \int_{P} d_{a} (U) d μ (a)$ for $P = Q, K$ . For every $x, a \in Q$ , insert $L_{x} L_{a} 1_{U}$ and use [F1] to obtain $d_{x} (U) \leq d_{a} (U) + d_{x a} (U)$ . Integrating over $a \in Q$ , left invariance and $x Q \subseteq K$ give $q d_{x} (U) \leq C_{Q} (U) + \int_{x Q} d_{b} (U) d μ (b) \leq C_{Q} (U) + C_{K} (U)$ . Therefore $\sup_{x \in Q} d_{x} (U) / μ (U) \leq (C_{Q} (U) + C_{K} (U)) / (q μ (U))$ . This scalar averaging inequality needs no identity in $Q$ , inverse-word cover, overlap inference or right-Haar factor.

3.1F1F3F5F6step 2.1constructalgebra

Choose a nonnegative finite-valued Borel representative of $h$ and put $U_{t} = {h > t}$ for $t > 0$ . By [F5], $H (t) = μ (U_{t}) \leq 1 / t < \infty$ ; it is nonincreasing and hence Borel measurable. If $s ↓ t$ , the sets $U_{s}$ increase to $U_{t}$ , so countable additivity gives $∥ 1_{U_{s}} - 1_{U_{t}} ∥_{1} \to 0$ . For each fixed $t$ , $D (a, t) = d_{a} (U_{t})$ is continuous in $a$ by [F1]. To prove product measurability, set $t_{n} (t) = 2^{- n} (⌊ 2^{n} t ⌋ + 1) > t$ , which decreases to $t$ . For each positive integer $j$ , $t_{n} (t) = j 2^{- n}$ on $[(j - 1) 2^{- n}, j 2^{- n}) \cap (0, \infty)$ ; thus a strict superlevel set of $D (a, t_{n} (t))$ is the countable union of the products of ${a : D (a, j 2^{- n}) > c}$ with these Borel intervals. The $a$ -sets are open by [F1], so $D (a, t_{n} (t))$ is product-measurable. The estimate $∣ D (a, t_{n} (t)) - D (a, t) ∣ \leq 2 ∥ 1_{U_{t_{n} (t)}} - 1_{U_{t}} ∥_{1}$ tends to zero uniformly in $a$ by [F1], so [F5] gives product measurability of $D$ . This constructs the bridge even when $G$ is not second countable; it does not treat arbitrary Borel functions on products as product-measurable.

4.1F2F3F4F5step 2.1step 3.1choosealgebra

For each $a$ , the strict-superlevel layer-cake identity [F4] gives $\int_{0}^{\infty} D (a, t) d t = ∥ L_{a} h - h ∥_{1}$ , while $\int_{0}^{\infty} H (t) d t = 1$ . Haar measure restricted to $Q$ and $K$ is finite; the level measure is sigma-finite, so product measurability from step 3.1 permits [F5] on each restricted product. For $F (t) = C_{Q} (U_{t}) + C_{K} (U_{t})$ this yields $\int_{0}^{\infty} F (t) d t \leq B : = δ (3 q / 2 + 2 k)$ by step 2.1. When $H (t) = 0$ , left invariance gives $F (t) = 0$ . There is a $t > 0$ with $H (t) > 0$ and $F (t) \leq B H (t)$ : otherwise the nonnegative measurable difference $F - B H$ would be strictly positive on ${H > 0}$ , a set of positive level measure since $\int H = 1$ , contradicting $\int (F - B H) \leq 0$ and [F2]. This also handles $δ = B = 0$ . Choose that $t$ and set $U = U_{t}$ .

5.1step 1.1step 2.2step 4.1algebra

With $r = k / q \geq 1$ , steps 2.2 and 4.1 give $\sup_{x \in Q} μ (x U △ U) / μ (U) \leq B / q = δ (3 / 2 + 2 r) \leq ε (1 + 3 / (4 r)) \leq 7 ε / 4 < 2 ε$ . Also $U$ is Borel and $0 < μ (U) < \infty$ by step 4.1. This proves the full original quantitative claim, including $δ = 0$ , with the stronger derived bound $7 ε / 4$ ; the stronger bound is a local conclusion, not an assertion about the cited source's identity-containing route.

6.1F3F6F7step 5.1construct∎

Finally assume (P1) and fix any compact target $T$ and $ε > 0$ . Choose a compact identity neighborhood $C$ by [F3] and put $Q_{0} = T \cup C$ . It is compact and has positive finite measure by [F3, F6]; so does $Q_{0}^{2}$ . Apply [F7] on $Q_{0}^{2}$ with tolerance $ε μ (Q_{0}) / (2 μ (Q_{0}^{2}))$ , and apply the just-proved quantitative clause to this density and $Q_{0}$ . The resulting $U$ satisfies the promised $2 ε$ bound on $Q_{0}$ , hence on $T$ . Empty $T$ has defect zero under the stated convention. Since the requested tolerance can also be replaced by half of any desired Følner tolerance, this is the full left Følner condition. No compact generation, countability or semifiniteness was used.

Remarks

The source extraction proofs begin with $e \in Q$ . Their overlap inference $μ (x Q^{2} \cap Q^{2}) \geq μ (Q)$ is false for an unqualified $Q$ : on the additive real line, $Q = [1, 2]$ and $x = 3 / 2$ give $Q^{2} = [2, 4]$ and $(x + Q^{2}) \cap Q^{2} = [7 / 2, 4]$ , of half the measure of $Q$ . Also for $Q = [100, 101]$ every $A \subseteq Q^{2} = [200, 202]$ has $A - A \subseteq [- 2, 2]$ , so $Q \subseteq A A^{- 1}$ is impossible. These examples refute that route, not the quantitative conclusion. The local proof above preserves the arbitrary-positive-compact- $Q$ claim by scalar left-Haar averaging and coarea after parity symmetrization, replacing the invalid overlap route without adding $e \in Q$ or changing the repository's Haar/null conventions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

173 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)