Finset and decidability

Stream: new members

[Laurent Bartholdi]

I'm trying to formalize bits of the theory of amenability of groups. Just to get started, I tried

import Mathlib.GroupTheory.GroupAction.Basic

variable {G α: Type _}
variable [Group G]
variable [MulAction G α]

def SetSetMul (S : Set G) (U : Set α) :=
  {gu : α | ∃g∈S, ∃u∈U, gu = g•u}

def FinsetFinsetMul (S : Finset G) (U : Finset α) : Finset α :=
  {gu : α | ∃g∈S, ∃u∈U, gu = g•u}

def IsAmenable : Prop :=
  ∀ε>0, ∀S : Finset G, ∃F : Finset α, (FinsetFinsetMul S F).card < (1+ε)*F.card

However, I already have a bunch of issues I don't know how to resolve:

1. FinsetFinsetMul chokes with the message failed to synthesize DecidablePred fun gu ↦ ∃ g ∈ S, ∃ u ∈ U, gu = g • u.
2. Do I have to type one version for Finset and one for Set in each definition?
3. Is there a more elegant notation for FinsetFinsetMul? My initial guess was {g•u | g∈S, u∈U}, but what compiles is more ugly

Thanks a lot!

[Sébastien Gouëzel]

If you open Pointwise, the right notation for SetSetMul is just S • U. Same thing for the finset version if you have suitable decidability assumptions around.

[Sébastien Gouëzel]

Like in

import Mathlib

variable {G α : Type*}
variable [Group G]
variable [MulAction G α]

open Pointwise

def SetSetMul (S : Set G) (U : Set α) := S • U

variable [DecidableEq α]

def FinsetFinsetMul (S : Finset G) (U : Finset α) : Finset α := S • U

def IsAmenable : Prop :=
  ∀ε>0, ∀S : Finset G, ∃F : Finset α, (S • F).card < (1+ε)*F.card

This means you should probably drop the definitions SetSetMul and FinsetFinsetMul and use the notation.

Note that your last epsilon is a natural number, which is probably not what you want...

[Laurent Bartholdi]

Great, thanks a lot!!!

Just to keep track of my progress, here's an easy lemma:

-- I had to explicitly pass G and  α as parameters, otherwise the next lemma can't figure out what the MulAction arguments are

def IsAmenable (G α : Type*) [Group G] [MulAction G α] [DecidableEq α] : Prop :=
  ∀ε>(0:ℝ), ∀S : Finset G, ∃F : Finset α, (S • F).card < (1+ε)*F.card

-- every action is on a finite, nonempty type is amenable
lemma FiniteAmenable (h0 : Nonempty α) (h1 : Fintype α) : IsAmenable G α := by
  intro ε ε_pos S
  let F := @Finset.univ α h1
  use F
  have sub : S • F ⊆ F := Finset.subset_univ _
  have carddec : ((S • F).card : ℝ) ≤ F.card := by gcongr
  apply lt_of_le_of_lt carddec
  have nonzero : F.card > (0 : ℝ) := Nat.cast_pos'.mpr Fintype.card_pos
  aesop

Comments on style are most welcome!

[Sébastien Gouëzel]

Here is a slightly amended version:

import Mathlib

open Pointwise

def IsAmenable (G α : Type*) [Group G] [MulAction G α] [DecidableEq α] : Prop :=
  ∀ε>(0:ℝ), ∀S : Finset G, ∃F : Finset α, (S • F).card < (1+ε)*F.card

variable {G α : Type*} [Group G] [MulAction G α] [DecidableEq α]

-- every action is on a finite, nonempty type is amenable
lemma isAmenable_of_fintype [Nonempty α] [Fintype α] : IsAmenable G α := by
  intro ε ε_pos S
  let F : Finset α := Finset.univ
  use F
  have sub : S • F ⊆ F := Finset.subset_univ _
  have carddec : ((S • F).card : ℝ) ≤ F.card := by gcongr
  apply lt_of_le_of_lt carddec
  have nonzero : (0 : ℝ) < F.card := Nat.cast_pos'.mpr Fintype.card_pos
  nlinarith

I haven't really touched your proof, but here are the cosmetical changes I made:

• I've made it self-contained (with imports and everything) so that it compiles out of the box for anyone opening it in the playground
• I've changed the name of the lemma, to follow the naming convention
• I've turned the nonemptiness and finiteness assumptions into typeclass assumptions: when applying the lemma, these will be filled in automatically by the system
• I've tweaked the definition of F, using the typeclass system to fill the assumption automatically
• I've changed the order of the inequality, from > to <: things just work better if everyone always uses the same direction in inequalities
• For the final step I use nlinarith (nonlinear arithmetic inequalities) instead of aesop (a general purpose tool, which here was probably just calling nlinarith)

[Luigi Massacci]

I don't think aesop can call nlinarith(?). I assume it will probably have made (the equivalent of) a giant simp soup of lt_iff... lemmas?