ExampleConstruction: Literature-sourcedVerification: 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 sets in $R^{n}$

Statement

Assume AC. Let $n \geq 1$ , let $G = R^{n}$ be the additive group with its Euclidean topology, and let $λ_{n}$ be Lebesgue measure. Then $λ_{n}$ is a left Haar measure on $G$ . For every compact $Q \subseteq R^{n}$ , choose $R \geq 0$ such that $Q \subseteq [- R, R]^{n}$ , and for $t > 0$ put $C_{t} : = [- t, t]^{n}$ . Then $Δ_{Q} (C_{t}) = \sup ({0} \cup {\frac{λ_{n} ((x + C_{t}) △ C_{t})}{λ_{n} (C_{t})} : x \in Q}) \leq 2 ((1 + R / t)^{n} - 1) \to_{t \to \infty}^{} 0,$ where $Δ_{Q}$ is the left Følner defect of Left Følner nets for locally compact groups. In particular $(C_{t})_{t > 0}$ is a left Følner net, $G$ satisfies the left Følner condition, and $R^{n}$ is amenable by The Følner criterion for locally compact groups.

Facts & Assumptions

Given: AC, an integer $n \geq 1$ , Euclidean $R^{n}$ with addition, Lebesgue measure $λ_{n}$ , and a compact $Q \subseteq R^{n}$ .

[A1]

AC is the choice-function principle and supplies countable choice (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

The Euclidean metric makes $R^{n}$ Hausdorff, addition is continuous by the metric triangle inequality and translation invariance, and inversion $x \mapsto - x$ is an isometry; $R^{n}$ is locally compact ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, Distinct points of a metric space have disjoint balls around them, Topological group: multiplication and inversion are continuous, $R^{n}$ is locally compact and $σ$ -compact).

[F2]

Under countable choice, the Lebesgue measurable sets form a sigma-algebra and $λ_{n}$ is a complete measure (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume); $λ_{n}$ is also Radon (Lebesgue measure is a Radon measure on R^n).

[F3]

Lebesgue measure and measurability are translation invariant; in particular $λ_{n} (x + E) = λ_{n} (E)$ for every Lebesgue-measurable set $E$ and vector $x$ (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[F4]

The closed box $[- t, t]^{n}$ and the expanded closed box $[- (t + R), t + R]^{n}$ are Borel measurable, with measures $(2 t)^{n}$ and $(2 (t + R))^{n}$ ; these are finite and the first is positive for $t > 0$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F5]

A measure is countably additive, hence finitely additive on disjoint measurable sets, and it is monotone under inclusion (Measures on sigma-algebras, Measures are monotone).

[F6]

Every compact subset of a metric space is bounded; boundedness means containment in some open metric ball. In $R^{n}$ , each coordinate obeys $∣ x_{j} ∣ \leq d_{2} (x, 0)$ , and $d_{2}$ satisfies the triangle inequality (A compact subset of a metric space is closed and bounded, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space, $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F7]

For a Borel set $F$ of positive finite Haar measure, the left Følner defect is $Δ_{Q} (F) = \sup ({0} \cup {μ (x F △ F) / μ (F) : x \in Q})$ , and it is zero for $Q = \emptyset$ ; a left Følner net is an eventually vanishing net of such sets (Left Følner nets for locally compact groups).

[F8]

A net is a function indexed by a nonempty directed preorder; $(0, \infty)$ with its usual order is directed (Directed preorders and nets).

[F9]

For $u \in [0, 1]$ and $n \geq 1$ , the binomial theorem gives $(1 + u)^{n} - 1 = \sum_{k = 1}^{n} ι (\binom{n}{k}) u^{k} \leq u \sum_{k = 1}^{n} ι (\binom{n}{k})$ , since each coefficient is nonnegative and $u^{k} \leq u$ (The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Integer powers $a^{m}$ , Finite sums and finite products, by recursion, Order on the reals).

[F10]

Under AC, amenability of an LCH group is equivalent to its satisfying the left Følner condition (The Følner criterion for locally compact groups).

[F11]

A left Haar measure is a nonzero Borel measure, finite on compact sets, Radon, and invariant under all left translations (Left Haar integral and left Haar measure).

Proof

Given: AC, $n \geq 1$ , Euclidean $R^{n}$ and its Lebesgue measure.

Proof technique: direct.

1.1F1construct

The metric formula in [F1] gives $d_{2} (x + y, x^{'} + y^{'}) \leq d_{2} (x, x^{'}) + d_{2} (y, y^{'})$ and $d_{2} (- x, - x^{'}) = d_{2} (x, x^{'})$ , so addition and inversion are continuous. By [F1], $R^{n}$ is a locally compact Hausdorff topological group.

2.1A1F2F3F4F11step 1.1construct

By [A1], countable choice is available for the Lebesgue Radon and box-volume results [F2, F4]. The box formula gives $λ_{n} ([- 1, 1]^{n}) = 2^{n} > 0$ , so $λ_{n}$ is nonzero; [F2] makes it Radon and [F3] makes it left invariant. With step 1.1, these are the Haar conditions of [F11], so $λ_{n}$ is a left Haar measure on $G$ .

2.2F6step 1.1construct

If $Q = \emptyset$ , choose $R = 0$ . Otherwise [F6] gives $x_{0} \in R^{n}$ and $r > 0$ with $Q \subseteq B_{2} (x_{0}, r)$ . Put $R : = r + d_{2} (x_{0}, 0) > 0$ . For $x \in Q$ and each $j < n$ , [F6] and the triangle inequality give $∣ x_{j} ∣ \leq d_{2} (x, 0) \leq d_{2} (x, x_{0}) + d_{2} (x_{0}, 0) < R$ , so $Q \subseteq [- R, R]^{n}$ .

3.1F2F3F4F5F7step 2.1step 2.2algebra

Fix $t > 0$ and $x \in Q$ , and put $A_{x} : = x + C_{t}$ . By [F2, F3, F4] the measurable sets $A_{x}$ and $C_{t}$ have equal finite measure $(2 t)^{n}$ . Their finite additive decompositions over $A_{x} \cap C_{t}$ therefore give $λ_{n} (A_{x} ∖ C_{t}) = λ_{n} (C_{t} ∖ A_{x})$ , hence $λ_{n} (A_{x} △ C_{t}) = 2 λ_{n} (A_{x} ∖ C_{t})$ . If $y \in A_{x} ∖ C_{t}$ , write $y = x + z$ with $z \in C_{t}$ ; since $x \in [- R, R]^{n}$ and $z \in [- t, t]^{n}$ , $y \in [- (t + R), t + R]^{n} ∖ C_{t}$ . By [F4, F5], this outer box minus $C_{t}$ has measure $(2 (t + R))^{n} - (2 t)^{n}$ , and monotonicity bounds $λ_{n} (A_{x} ∖ C_{t})$ by that value. Dividing by $(2 t)^{n} > 0$ yields $λ_{n} (A_{x} △ C_{t}) / λ_{n} (C_{t}) \leq 2 ((1 + R / t)^{n} - 1)$ . The bound is uniform in $x \in Q$ , and when $Q = \emptyset$ the defect is zero by [F7], proving the displayed inequality for every $Q$ and $t > 0$ .

4.1F4F6F7F8F9step 2.2step 3.1algebra

Every $C_{t}$ is a closed, hence Borel, box with $0 < λ_{n} (C_{t}) = (2 t)^{n} < \infty$ by [F4], so [F8] indexes a left Følner net by $t \in (0, \infty)$ . Fix compact $Q$ and $ε > 0$ , and use [F6] to choose its bound $R$ as in step 2.2. If $R = 0$ , then every $x \in Q$ equals $0$ and the defect is zero. If $R > 0$ , put $S_{n} : = \sum_{k = 1}^{n} ι (\binom{n}{k})$ and $T : = 1 + R + 2 S_{n} R / ε$ . For $t \geq T$ , $u : = R / t \in (0, 1]$ , so [F9] and step 3.1 give $Δ_{Q} (C_{t}) \leq 2 S_{n} R / t \leq ε$ . Thus the net is eventually Følner on every compact $Q$ , and $R^{n}$ satisfies the left Følner condition.

5.1A1F10step 4.1given∎

By [F10], the left Følner condition proved in step 4.1 implies amenability under the stated AC. Hence $R^{n}$ has all the properties in the Statement.

Sources

BHV, Kazhdan's Property (T), Appendix G.5 Theorem G.5.1 and its complete proof (printed pp. 466–469) give the general locally compact Følner criterion. Example G.5.4 (printed p. 469) concerns intervals in $Z$ , not cubes in $R^{n}$ . Garrido, An Introduction to Amenable Groups, §3.1 Definition 3.1 and Example 3.5 discuss the discrete condition and intervals in $Z$ ; they provide context only. The Euclidean cube estimate and the one-sided-shell calculation are proved locally here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

144 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) (Cambridge University Press, 2008; author-hosted complete text) (standard reference, not scraped)
Jose Manuel Garcia Garrido, An Introduction to Amenable Groups (author-hosted lecture notes, University of Duesseldorf) (standard reference, not scraped)

Følner sets in RnRn

Statement

Facts & Assumptions

Proof

Sources

Depends on

Used by

Dependency tree · two levels

Sources

Følner sets in $R^{n}$