MeanToFolner.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ThompsonNonamenability.InvariantMean.exists_folner_total line 17
Source documentation
A standard invariant mean yields a finite set with small total boundary.
```
theorem InvariantMean.exists_folner_total (M : InvariantMean G)
    (S : Finset G) {ε : ℝ} (hε : 0 < ε) :
    ∃ A : Finset G, A.Nonempty ∧
      (∑ h ∈ S, ((leftTranslate h A ∆ A).card : ℝ)) < ε * A.card := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.leftTranslate
theorem OAI.ThompsonNonamenability.InvariantMean.exists_folner line 33
Source documentation
Finite Følner sets, with no countability or finite-generation assumption.
```
theorem InvariantMean.exists_folner (M : InvariantMean G)
    (S : Finset G) {ε : ℝ} (hε : 0 < ε) :
    ∃ A : Finset G, A.Nonempty ∧
      ∀ h ∈ S, ((leftTranslate h A ∆ A).card : ℝ) < ε * A.card := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.leftTranslate
theorem OAI.ThompsonNonamenability.not_amenable_of_uniform_boundary line 47
Source documentation
Uniform expansion of nonempty finite sets rules out a standard invariant mean.
```
theorem not_amenable_of_uniform_boundary (S : Finset G) {b : ℝ} (hb : 0 < b)
    (hexpand : ∀ A : Finset G, A.Nonempty →
      ∃ h ∈ S, b * A.card ≤ ((leftTranslate h A ∆ A).card : ℝ)) :
    ¬ Nonempty (InvariantMean G) := by
…
```
Mentions: OAI.ThompsonNonamenability.leftTranslate, OAI.ThompsonNonamenability.InvariantMean