MeanApproximation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite probabilities approximately invariant under a finite set

The usual positive normalized invariant mean forces zero to lie in the closure of the actual finite-probability defect set. The separation argument uses bounded coordinate functions of a continuous linear functional on ℓ¹; no identification of the full dual of ℓ¹ is assumed.

def OAI.ThompsonNonamenability.separatorCoordinate line 31
Source documentation
A separator gives one bounded real function for each translation.
```
def separatorCoordinate {S : Finset G} (ell : DefectSpace S →L[ℝ] ℝ)
    (h : {h : G // h ∈ S}) : BoundedReal G :=
…
```
Mentions: OAI.ThompsonNonamenability.DefectSpace, OAI.ThompsonNonamenability.BoundedReal
theorem OAI.ThompsonNonamenability.separatorCoordinate_apply line 41
def OAI.ThompsonNonamenability.separatorDefect line 46
Source documentation
The finite sum whose mean vanishes by left invariance.
```
def separatorDefect {S : Finset G} (ell : DefectSpace S →L[ℝ] ℝ) : BoundedReal G :=
…
```
Mentions: OAI.ThompsonNonamenability.DefectSpace, OAI.ThompsonNonamenability.BoundedReal
theorem OAI.ThompsonNonamenability.separatorDefect_apply line 50
theorem OAI.ThompsonNonamenability.InvariantMean.separatorDefect_eq_zero line 58
theorem OAI.ThompsonNonamenability.InvariantMean.zero_mem_closure_defectSet line 66
Source documentation
Separation contradicts the existence of a positive normalized invariant mean.
```
theorem InvariantMean.zero_mem_closure_defectSet (M : InvariantMean G)
    (S : Finset G) : (0 : DefectSpace S) ∈ closure (defectSet S) := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.DefectSpace, OAI.ThompsonNonamenability.defectSet
theorem OAI.ThompsonNonamenability.InvariantMean.exists_probability_small_defect line 87
Source documentation
Actual nonnegative finite probabilities with arbitrarily small total defect.
```
theorem InvariantMean.exists_probability_small_defect (M : InvariantMean G)
    (S : Finset G) {ε : ℝ} (hε : 0 < ε) :
    ∃ p : G →₀ ℝ, IsProbabilityWeights p ∧ ‖defectMap S p‖ < ε := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.IsProbabilityWeights, OAI.ThompsonNonamenability.defectMap