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.

Left-invariant means on $L^{\infty}$ of a locally compact group

Definition

Let $G$ be a locally compact Hausdorff group with fixed left Haar measure $μ$ . Write $L^{\infty} (G) : = L^{\infty} (G, μ; C)$ for the complex a.e.-class space of Complex $L^{\infty}$ space of a locally compact group. For $g \in G$ define the left translate by $L_{g} f (x) : = f (g^{- 1} x) .$ It is well defined on classes and isometric, and $L_{g_{1}} L_{g_{2}} = L_{g_{1} g_{2}}$ .

For a bounded complex-linear functional, write $∥ m ∥ : = \sup {∣ m (f) ∣ : ∥ f ∥_{\infty} \leq 1}$ for its operator norm.

A mean on $L^{\infty} (G)$ is a complex-linear functional $m : L^{\infty} (G) \to C$ such that $m (f) \geq 0$ whenever $f \geq 0$ and $m (1_{G}) = 1$ , where $1_{G}$ is the class of the constant-one function. It is left invariant if $m (L_{g} f) = m (f)$ for every $g \in G$ and $f \in L^{\infty} (G)$ . Every mean has operator norm one and satisfies $∣ m (f) ∣ \leq m (∣ f ∣) \leq ∥ f ∥_{\infty} .$ Equivalently, a mean is a positive complex-linear functional of norm one.

Facts & Assumptions

Given: A locally compact Hausdorff group $G$ with fixed left Haar measure $μ$ and the complex normed space $L^{\infty} (G)$ .

[A1]

The left Haar measure is a nonzero Borel measure and satisfies $μ (g E) = μ (E)$ for every Borel set $E \subseteq G$ and $g \in G$ (Left Haar integral and left Haar measure).

[F1]

The elements of $L^{\infty} (G)$ are complex measurable functions modulo almost-everywhere equality; its operations are well defined, its norm is the essential supremum, and it is a complex normed vector space (Complex $L^{\infty}$ space of a locally compact group).

[F2]

Left translation $x \mapsto g^{- 1} x$ is a homeomorphism of $G$ ; a continuous map has Borel preimages of Borel sets (Topological group: multiplication and inversion are continuous, Group and abelian group, A continuous map has Borel preimages of Borel sets, The Borel sigma-algebra of a topological space).

[F3]

Complex conjugation, real and imaginary parts, and the modulus have their coordinate definitions and conjugation/multiplicativity laws, including $z \overline{z} = ∣ z ∣^{2}$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , and $∣ \overline{z} ∣ = ∣ z ∣$ (Real and imaginary parts, complex conjugation, and modulus, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F4]

For $z = a + b i$ , $∣ Re z ∣ = ∣ a ∣ \leq \sqrt{a^{2} + b^{2}} = ∣ z ∣$ ; the inequality follows because $b^{2} \geq 0$ and squaring is monotone on the nonnegative reals (Basic properties of the absolute value, Squaring is monotone on the nonnegatives, Squares of nonzero elements are positive).

Proof

technique · direct

1.1A1F1F2constructalgebra

For $g \in G$ , the composition $x \mapsto f (g^{- 1} x)$ is Borel measurable by [F2]. If $f = f^{'}$ outside a Borel null set $N$ , then $L_{g} f = L_{g} f^{'}$ outside $g N$ , which is null by [A1]; thus $L_{g}$ is well defined on a.e. classes. For each $t > 0$ , ${x : ∣ L_{g} f (x) ∣ > t} = g {y : ∣ f (y) ∣ > t}$ , so [A1] preserves every superlevel-set measure and hence the essential-supremum norm. Direct calculation gives $L_{e} = I$ and $L_{g_{1}} L_{g_{2}} = L_{g_{1} g_{2}}$ .

1.2F1F3F4givenalgebra

Let $m$ be a positive complex-linear functional on $L^{\infty} (G)$ . If $u$ is real-valued, write $u = u_{+} - u_{-}$ with $u_{+} = (u + ∣ u ∣) / 2$ and $u_{-} = (- u + ∣ u ∣) / 2$ , so $u_{+}, u_{-} \geq 0$ and both remain in $L^{\infty} (G)$ by [F1, F3]. Positivity makes $m (u_{+})$ and $m (u_{-})$ real, so $m (u)$ is real. Thus, writing $f = Re f + i Im f$ , one has $m (\overline{f}) = \overline{m (f)}$ . If $m (f) \neq 0$ , set $α : = \overline{m (f)} / ∣ m (f) ∣$ . By [F3], $∣ α ∣ = 1$ and $m (Re (α f)) = Re (α m (f)) = ∣ m (f) ∣$ ; since $Re (α f) \leq ∣ α f ∣ = ∣ f ∣$ by [F3, F4], positivity gives $∣ m (f) ∣ \leq m (∣ f ∣)$ . This inequality is immediate as well when $m (f) = 0$ .

2.1A1F1step 1.2givenalgebra∎

The constant-one class has norm one: $μ (G) > 0$ by nonzeroness in [A1], so its superlevel set is $G$ for $0 < t < 1$ and empty for $t \geq 1$ . For every $ϵ > 0$ , the essential-supremum definition [F1] gives $∣ f ∣ \leq (∥ f ∥_{\infty} + ϵ) 1_{G}$ almost everywhere. If $m$ is positive, then $m (1_{G}) \geq 0$ and $m (∣ f ∣) \leq (∥ f ∥_{\infty} + ϵ) m (1_{G})$ ; letting $ϵ$ decrease to zero and using step 1.2 yields $∣ m (f) ∣ \leq ∥ f ∥_{\infty} m (1_{G})$ , so $m$ is bounded. Taking the supremum on the unit ball and testing at $1_{G}$ shows $∥ m ∥ = m (1_{G})$ . Consequently positivity and $m (1_{G}) = 1$ imply $∥ m ∥ = 1$ , and positivity with $∥ m ∥ = 1$ implies $m (1_{G}) = 1$ . For a mean this also gives $∣ m (f) ∣ \leq m (∣ f ∣) \leq ∥ f ∥_{\infty}$ .

Depends on

Used by

Dependency tree · two levels

41 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 Folner 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)

Left-invariant means on L∞L∞ of a locally compact group