Amenable groups
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremTauCeti.Amenable.of_hasFoelnerSets#
A group with Følner sets is amenable, for every group topology.
TauCeti.Amenable.of_hasFoelnerSets.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] (h : TauCeti.HasFoelnerSets G) : TauCeti.Amenable G
Uses 3 · Used by 1
TheoremTauCeti.Amenable.of_tendsto#
Cluster-point criterion: a topological group is amenable when it carries means ms i which
are approximately left invariant along a nontrivial filter, that is, ms i (L_g f) - ms i f → 0
for every g and f.
TauCeti.Amenable.of_tendsto.{u_1, u_2} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {ms : ι → TauCeti.Mean G}
(h :
∀ (g : G) (f : TauCeti.UCB G),
Filter.Tendsto (fun i => (ms i) ((TauCeti.UCB.leftTranslation g) f) - (ms i) f) l (nhds 0)) :
TauCeti.Amenable G
Uses 3 · Used by 1
TheoremTauCeti.amenable_iff_forall_finset_exists#
Finite-intersection criterion: a topological group is amenable exactly when every finite
family of invariance equations m (L_g f) = m f is satisfied by some mean.
TauCeti.amenable_iff_forall_finset_exists.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] :
TauCeti.Amenable G ↔
∀ (s : Finset (G × TauCeti.UCB G)),
∃ m, ∀ p ∈ s, m ((TauCeti.UCB.leftTranslation p.1) p.2) = m p.2
Uses 3 · Used by 2
TheoremTauCeti.Amenable.of_directed_of_iSup_eq_top#
A topological group which is the union of a nonempty directed family of amenable subgroups is amenable.
TauCeti.Amenable.of_directed_of_iSup_eq_top.{u_1, u_2} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] {ι : Type u_2} [Nonempty ι] {H : ι → Subgroup G}
(hH : Directed (fun x1 x2 => x1 ≤ x2) H) (htop : ⨆ i, H i = ⊤)
[∀ (i : ι), TauCeti.Amenable ↥(H i)] : TauCeti.Amenable G
Uses 3
TheoremTauCeti.Amenable.of_isColimit#
The apex of a colimit cocone over a filtered diagram of amenable topological groups in GrpCat
is amenable, provided the legs of the cocone are continuous.
TauCeti.Amenable.of_isColimit.{u, v_1, u_1} {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J]
[CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J GrpCat}
[(j : J) → TopologicalSpace ↑(F.obj j)] {c : CategoryTheory.Limits.Cocone F}
[TopologicalSpace ↑c.pt] [IsTopologicalGroup ↑c.pt] [∀ (j : J), IsTopologicalGroup ↑(F.obj j)]
[∀ (j : J), TauCeti.Amenable ↑(F.obj j)] (hc : CategoryTheory.Limits.IsColimit c)
(hcont : ∀ (j : J), Continuous ⇑(GrpCat.Hom.hom (c.ι.app j))) : TauCeti.Amenable ↑c.pt
Uses 3
TheoremReiter implies Følner#
If a nonnegative finitely supported function p on X satisfies
∑_{g ∈ K} ∑_x |p (g⁻¹ • x) - p x| < ε · ∑_x p x, then some finite nonempty set F ⊆ X satisfies
|g • F ∆ F| < ε |F| for every g ∈ K.
TauCeti.exists_finset_card_smul_symmDiff_lt_of_sum_tsum_lt.{u_1, u_2} {G : Type u_1} {X : Type u_2}
[Group G] [MulAction G X] [DecidableEq X] {p : X → ℝ} (hp : 0 ≤ p)
(hfin : Function.HasFiniteSupport p) {K : Finset G} {ε : ℝ}
(h : ∑ g ∈ K, ∑' (x : X), |p (g⁻¹ • x) - p x| < ε * ∑' (x : X), p x) :
∃ F, F.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card
Lean
Formalized in Tau Ceti as TauCeti.exists_finset_card_smul_symmDiff_lt_of_sum_tsum_lt.
Sources
Used by 1
TheoremTauCeti.Amenable.of_finite#
A finite topological group is amenable, for any group topology.
TauCeti.Amenable.of_finite.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] [Finite G] : TauCeti.Amenable G
Uses 2
TheoremTauCeti.Mean.isLeftInvariant_iff_eq_uniform#
On a finite group, the uniform mean is the unique left-invariant mean.
TauCeti.Mean.isLeftInvariant_iff_eq_uniform.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] [Finite G] {m : TauCeti.Mean G} :
m.IsLeftInvariant ↔ m = TauCeti.Mean.uniform G
Uses 1
ClassTauCeti.Amenable#
A topological group G is amenable when UCB G carries a left-invariant mean.
TauCeti.Amenable.{u_1} (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop
Uses 1 · Used by 7
DefinitionTauCeti.UCB.leftTranslation#
Left translation g ↦ L_g, where (L_g f)(x) = f (g⁻¹ * x), as a group homomorphism from G
to the linear isometry equivalences of UCB G; the case 𝕜 = ℝ of
ucbSubalgebra.leftTranslation.
TauCeti.UCB.leftTranslation.{u_2} {G : Type u_2} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] : G →* TauCeti.UCB G ≃ₗᵢ[ℝ] TauCeti.UCB G
Used by 9
TheoremTauCeti.Mean.instCompactSpace#
The space of means is weak-* compact.
TauCeti.Mean.instCompactSpace.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] : CompactSpace (TauCeti.Mean G)
Used by 2
TheoremEquidecompositions as partitions#
Two sets A and B are related by an
equidecomposition exactly when there are a finite partition of A and a group element γ s for
each part s, such that the translates γ s • s are pairwise disjoint with union B.
Equidecomp.exists_iff_exists_finpartition.{u_1, u_2} {X : Type u_1} {G : Type u_2} [Group G]
[MulAction G X] {A B : Set X} :
(∃ f, f.source = A ∧ f.target = B) ↔
∃ P γ, ((↑P.parts).PairwiseDisjoint fun s => γ s • s) ∧ ⋃ s ∈ P.parts, γ s • s = B
Uses 1 · Used by 1
StructureEquidecomp.Equipartition#
An equipartition of X for an action of G: a finite set of pairs (Aᵢ, gᵢ) of a nonempty
source piece Aᵢ : Set X and a group element gᵢ : G, such that the source pieces Aᵢ are
pairwise disjoint and the target pieces gᵢ • Aᵢ are pairwise disjoint. When G is a group
acting on X, moving each Aᵢ by gᵢ is then an equidecomposition of the union of the Aᵢ with
the union of the gᵢ • Aᵢ (see Equidecomp.Equipartition.toEquidecomp).
Equidecomp.Equipartition.{u_1, u_2} (X : Type u_1) (G : Type u_2) [SMul G X] : Type (max u_1 u_2)
Used by 1
TheoremTauCeti.hasFoelnerSets_iff#
A group has Følner sets exactly when for every finite K ⊆ G and every ε > 0 there is a
finite nonempty F ⊆ G with |gF △ F| < ε · |F| for all g ∈ K.
TauCeti.hasFoelnerSets_iff.{u_1} {G : Type u_1} [Group G] [DecidableEq G] :
TauCeti.HasFoelnerSets G ↔
∀ (K : Finset G) (ε : ℝ),
0 < ε → ∃ F, F.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card
Used by 1
TheoremSchröder–Bernstein theorem for equidecompositions#
If each of A and B is
equidecomposable with a subset of the other, then A and B are equidecomposable.
TauCeti.EquidecomposableLE.antisymm.{u_1, u_3} {X : Type u_1} {G : Type u_3} [Group G]
[MulAction G X] {A B : Set X} (hAB : TauCeti.EquidecomposableLE G A B)
(hBA : TauCeti.EquidecomposableLE G B A) : TauCeti.Equidecomposable G A B
Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.