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.

Compact groups have a constant Reiter net

Statement

Assume AC. Let $K$ be a compact locally compact Hausdorff group. Choose a left Haar measure $ν$ on $K$ and put $μ : = ν / ν (K)$ ; the denominator is positive and finite, so $μ$ is a normalized Haar probability. Let $f : = 1_{K} \in L^{1} (K)$ . Then $f \geq 0$ , $∥ f ∥_{1} = 1$ , and $L_{x} f = f$ for every $x \in K$ , because $L_{x} 1_{K} = 1_{x K} = 1_{K}$ . Hence the constant net $f_{i} : = f$ satisfies Reiter's condition (P1) exactly, with $Δ_{Q} (f) = 0$ for every compact $Q \subseteq K$ , and $K$ is amenable by Amenability is equivalent to Reiter's condition (P1). This is the strongest possible form of approximate invariance: the approximating densities do not vary with the tolerance.

Facts & Assumptions

Given: AC and a compact locally compact Hausdorff group $K$ .

[A1]

AC is the choice-function principle (The Axiom of Choice).

[F1]

Under AC, a locally compact Hausdorff group has a left Haar measure $ν$ (Existence of left and right Haar measures, Left Haar integral and left Haar measure). A compact group $K$ is open in itself and compact, so $0 < ν (K) < \infty$ (Haar measure is positive on nonempty open sets and finite on compact sets); the rescaling $μ : = ν / ν (K)$ is left Haar and satisfies $μ (K) = 1$ .

[F2]

Left translations $T_{x} (y) = x^{- 1} y$ are Borel and preserve left Haar measure, and integration is invariant under measure-preserving maps (Left Haar integral and left Haar measure, Measure-preserving transformations and systems, A continuous map has Borel preimages of Borel sets, Integral invariance under measure-preserving maps).

[F3]

Complex $L^{1} (K)$ consists of almost-everywhere classes with $∥ g ∥_{1} = \int_{K} ∣ g ∣ d μ$ ; a nonnegative indicator has integral equal to the measure of its set (Complex Haar L^p spaces and compactly supported functions, Integrable real and complex functions, and their integrals, The nonnegative Lebesgue integral, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions).

[F4]

Complex $L^{\infty} (K)$ consists of Borel almost-everywhere classes with finite essential supremum; for every $φ \in L^{\infty} (K)$ and $η > 0$ , $∣ φ ∣ \leq ∥ φ ∥_{\infty} + η$ almost everywhere (Complex $L^{\infty}$ space of a locally compact group, The essential supremum of a measurable function with respect to a measure).

[F5]

Since $μ (K) = 1$ , every $φ \in L^{\infty} (K)$ is integrable: the essential bound in [F4] gives $\int_{K} ∣ φ ∣ d μ \leq (∥ φ ∥_{\infty} + η) μ (K) < \infty$ for any $η > 0$ ; order and scalar rules for the nonnegative integral apply (Integrable real and complex functions, and their integrals, Monotonicity and nonnegative homogeneity of the nonnegative integral, [F1, F4]).

[F6]

The complex integral is independent of the representative modulo almost- everywhere equality and is complex-linear on $L^{1}$ (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree, The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F7]

Reiter (P1) requires, for every compact $Q$ and $ε > 0$ , a nonnegative $L^{1}$ class of norm one with $Δ_{Q} (f) \leq ε$ ; the empty-test defect is zero (Reiter's condition (P1)).

[F8]

Under AC, Reiter (P1) implies amenability (Amenability is equivalent to Reiter's condition (P1)).

[F9]

A mean on complex $L^{\infty} (K)$ is a positive complex-linear functional with value one on the constant-one class, and amenability is existence of a left-invariant such mean (Left-invariant means on $L^{\infty}$ of a locally compact group, Amenable locally compact group).

[F10]

A singleton with its unique preorder is a nonempty directed set and therefore indexes a net (Directed preorders and nets).

[F11]

The compact-group clause records that every compact LCH group is amenable (Compact and locally compact abelian groups are amenable).

Proof

Given: AC, the compact LCH group $K$ , and its normalized left Haar probability $μ$ .

Proof technique: direct.

1.1A1F1F3F7construct

By [A1, F1], choose left Haar $ν$ and set $μ : = ν / ν (K)$ ; since [F1] gives $0 < ν (K) < \infty$ , positive scalar rescaling preserves left Haar properties and $μ (K) = 1$ . Set $f = 1_{K}$ . It is Borel and nonnegative, and [F3] gives $∥ f ∥_{1} = \int_{K} 1_{K} d μ = μ (K) = 1$ , so $f \in P$ . For every $x, y \in K$ , $L_{x} f (y) = f (x^{- 1} y) = 1 = f (y)$ because $x^{- 1} y \in K$ . Thus $L_{x} f = f$ as an $L^{1}$ class and $∥ L_{x} f - f ∥_{1} = 0$ for every $x \in K$ ; in particular $Δ_{Q} (f) = 0$ for every compact $Q$ , including $Q = \emptyset$ .

2.1A1F7F8F10step 1.1construct

By [F10], the singleton $I = {*}$ with its unique preorder is directed; set $f_{*} : = f$ . For every compact $Q \subseteq K$ and $ε > 0$ , step 1.1 gives $Δ_{Q} (f_{*}) = 0 \leq ε$ , so this constant net witnesses Reiter (P1) by [F7]. The Reiter equivalence [F8], under the stated AC, proves that $K$ is amenable.

3.1A1F1F2F3F4F5F6F9F11step 2.1algebra∎

Define $m ([φ]) : = \int_{K} φ d μ$ on complex $L^{\infty} (K)$ . By [F5] every such class is integrable; [F6] makes the value independent of the representative and complex-linear. If $[φ] \geq 0$ , its nonnegative representative has nonnegative integral, so $m$ is positive by [F3]; and $m (1_{K}) = μ (K) = 1$ by [F1] and [F3]. For $x \in K$ , [F2] gives $m (L_{x} [φ]) = \int_{K} φ (x^{- 1} y) d μ (y) = \int_{K} φ d μ$ for every $[φ] \in L^{\infty} (K)$ . Thus $m$ is a left-invariant mean in the sense of [F9], explicitly realizing the compact-group amenability clause of [F11] under the library's complex $L^{\infty}$ convention. The local calculation verifies the normalized-Haar mean on all $L^{\infty}$ classes.

Sources

BHV, Kazhdan's Property (T), Appendix G.1 Example G.1.5 (printed p. 448) identifies normalized Haar probability as the invariant mean on $C (K)$ and concludes compact groups are amenable. Appendix G.3 Theorem G.3.1(iii) (printed pp. 452–453) states Reiter (P1) for compact test sets. The local calculation extends the normalized-Haar mean to the library's complex $L^{\infty}$ classes.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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