Commit 2026-01-13 15:36 0483fb67

feat(MeasureTheory): Foelner filters (#31653) 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.