Amenable Groups

Stream: new members

[Matthias U]

Hi, I've been writing an implementation of amenable (discrete) groups (via the existence of left-invariant menas). It now contains quite some files, as I treat various inheritance properties, a proof that finite groups are amenable and amenability via Folner sequences.

Where should I place these files? Is making a folder group_theory/amenable a good idea?

As pull-requests should be small, self-contained pieces, (how) should I split up the work into pull requests? Is it ok to make a single pull request or should I make requests for each single file? (The project is rather self-contained and only relies on things that have already been accepted into the mathlib).

[Yaël Dillies]

One PR per file is a good guideline, yes.

[Notification Bot]

Matthias U has marked this topic as unresolved.

[Matthias U]

Junyan Xu said:

As for lemmas in aux_lemmas_sums.lean, sum_scalar is docs#finset.mul_sum, and symm_diff_of_diff_sum is docs#finset.sum_sdiff_sub_sum_sdiff.

Thanks! I deleted aux_lemmas_sums and replaced the occurences by docs#finset.mul_sum, etc

[Matthias U]

Junyan Xu said:

Regarding the definition of mean:

• instead of using continuous_bounded_function, you may use l^infty via docs#lp, so you don't need to deal with continuity at all. (Of course it would be nicer if we generalize from discrete groups to locally compact Hausdorff groups, where we'd consider the L^infty space w.r.t. the Haar measure (see Wikipedia).)

Your're right. I feel like I should state this for docs#topological_group . (I just rewrote the definition to topological groups)

[Matthias U]

Junyan Xu said:

Regarding the definition of mean:

• instead of using the existence of an invariant mean on the space of bounded functions as the main definition, we may use the existence of an invariant finitely additive measure, which seems simpler. The mean could be obtained by "Lebesgue integration" and the mathlib version requires a countably-additive measure, probably because we don't have finitely-additive measure as a def? Is a refactor in order?

I mainly chose the definition via invariant means because I felt that it would be easier to prove that extensions of amenable groups by amenable groups are amenable (see PR #16578) using this definition, rather than using the existence of finitely additive, invariant measures.

[Junyan Xu]

I just opened #16601 which allows you to replace positivity by monotonicity. But to make use of that, we need the partial order on the function space. We actually have docs#bounded_continuous_function.partial_order, so in your current setting you can directly do the replacement. However I think using continuous function is morally wrong: if you only want to deal with discrete groups you should use docs#lp and for the general case you should use docs#measure_theory.Lp with docs#measure_theory.measure.haar_measure (with p = ⊤, i.e. infinity); in either case, continuous functions don't show up. However, these spaces apparently don't have partial order instances on them; for docs#lp it would be easy and for docs#measure_theory.Lp we could just transfer the instance docs#measure_theory.ae_eq_fun.partial_order. Maybe we should also generalize the theory of means to function spaces that has_one. Let me tag @Yaël Dillies for his insights.

There are currently six open PRs about amenable groups, and we should first focus on #16574 to get the basic definitions fixed. Many proofs could be golfed (for mathematically trivial proofs we prefer one-line rw/simp proofs instead of calc), but not before we agree upon the fundamental design.

[Rémy Degenne]

I did not look at those PRs so I am not sure of what you need but we do have some order properties for Lp. See docs#measure_theory.Lp.normed_lattice_add_comm_group and other lemmas in the lp_order file.

[Junyan Xu]

Thanks! I only looked for partial_order and I'm glad to learn about the existence of the stronger bundled instance!

Personally I find the noncanonical docs#measure_theory.ae_eq_fun.has_coe_to_fun very strange. Do you know what it's useful for?

[Rémy Degenne]

It makes sure that the function you get is strongly measurable

[Kalle Kytölä]

Junyan Xu said:

• instead of positivity you may use docs#monotone, but mathlib doesn't seem to have the fact that monotonicity is equivalent to positivity for ordered add_groups. This is related to positive linear functionals; by the way do we have the Riesz–Markov–Kakutani representation theorem?

Hey, sorry for not giving the updates on this one! @Jesse Reimann has a sorry-free proof of the Riesz-Markov-Kakutani representation theorem for compact Hausdorff spaces. :tada:

(I imagine many people will instinctively feel like mathlib should have the locally compact generality at once, but I would argue that the compact case should have a separate implementation because several minor things connect to different existing things in a genuinely different/stronger way than in the locally compact case.)

The fact that Jesse was working on this was discussed here. We forgot to announce the completion of the proof, but that's indeed done. I hope that after some cleaning up, this could also lead to PRs of the Riesz-Markov-Kakutani to mathlib.