feat(MeasureTheory): Foelner filters

[ster99]

Define a predicate for a filter to be Foelner. Prove that if a measure space with a G-action has a Foelner filter then there is a left-invariant finitely additive probability measure on it (amenability).

Define the maximal Foelner filter and prove that if the maximal Foelner filter is nontrivial, then the amenability condition above holds.

Closes #29213.

---

depends on : #32117.

[github-actions]

PR summary 9aa5b55969

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.FoelnerFilter (new file)	1251

---

Declarations diff

+ IsFoelner
+ IsFoelner.amenable
+ IsFoelner.mean
+ IsFoelner.mean_smul_eq_mean
+ IsFoelner.mean_union_eq_add_of_disjoint
+ IsFoelner.mean_univ_eq_one
+ IsFoelner.mono
+ IsFoelner.tendsto_nhds_mean
+ IsFoelner.univ_of_isFiniteMeasure
+ amenable_of_maxFoelner_ne_bot
+ isFoelner_iff_tendsto
+ maxFoelner

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ADedecker]

Here is a question: in the context of topological groups, another possible condition would be to ask for this convergence to be uniform on compact sets. It turns out that (at least for the group acting on itself) one can always get a Foelner filter in this strong sense from amenability, which is implied by the existence of a Foelner filter in the weak sense. How do we plan to state these two notions?

I'm perfectly fine with leaving this for later, just gathering opinions.

[ster99]

I would probably go (already in the indexed notation) for a different structure IsUniformFoelner (l : Filter ι) (F : ι → Set X) with, instead of tendsto_meas_symmDiff, tendsto_meas_symmDiff_uniform (K : Set G) (hK : IsCompact K) : Tendsto (fun i ↦ ⨆ (g : G) (_ : g ∈ K), μ ((g • (F i)) ∆ (F i)) / μ (F i)) l (𝓝 0). And then a "cast" IsUniformFoelner.to_IsFoelner.

For what is worth, in my opinion extending the structure IsFoelner is not a good idea here.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[ADedecker]

I know this isn't ready for review yet, but here is a suggestion: I think you should add a lemma stating that IsFoelner stays true when you make the filter finer. Then, instead of writing the limUnder all the time, I would suggest defining IsFoelner.mean which gives the mean associated to a Foelner ultrafilter. Having a definition should make it easier to write and prove facts about it.

[ster99]

I would also like to draw your attention to the following point. In the lemma IsFoelner.mean_add_of_ultrafilter_le, where I prove finite additivity, I require measurability of at least one of the sets. I arbitrarily chose to assume MeasurableSet t, without any particular justification. How should I proceed? If I ask also for MeasurableSet s the hypothesis would not be used in the proof which does not seem the right way to go

[ADedecker]

Thanks, this is starting to look really good!

I don't think you have to worry about the measurability thing. The fact that MeasureTheory.measure_union holds with only one measurability is a nice trick, but morally the right assumption is that everything is measurable anyways.

[ADedecker]

I think you should hide this in a lemma about IsFoelner.mean, which would say, given an ultrafilter and an IsFoelner hypothesis, that fun i ↦ μ (s ∩ (F i)) / μ (F i) indeed tends to IsFoelner.mean μ u.toFilter F s along u.

[ster99]

I tried to avoid that part, however I only found tendsto_nhds_limUnder, which I guess is what you are asking for. However it requires a proof that there exists a limit point, which is exactly what the tendsto_of_eventually_mem_isCompact makes up for

[ster99]

Nevermind, I see what you meant

[ADedecker]

Oh I missed that this was still "awating-author" 🤦
Sorry if you intended to do more work before getting another look.

[ster99]

It's fine, I did not put that label and I am not sure how to get rid of it. Give as many looks as you like, it is very much appreciated!