FolnerInvariantMean.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite Følner averages yield the invariant mean for height correction

def OAI.PolycyclicRecognition.finiteMeanState line 19
Source documentation
A literal uniform average over a finite set, as a linear functional on the actual space of bounded real functions.
```
def finiteMeanState (A : Finset G) : BoundedReal G →ₗ[ℝ] ℝ where
…
```
theorem OAI.PolycyclicRecognition.finiteMeanState_positive line 25
theorem OAI.PolycyclicRecognition.finiteMeanState_one line 30
theorem OAI.PolycyclicRecognition.finiteMeanState_translation_bound line 35
Source documentation
The translation defect is bounded by the actual symmetric-difference ratio times the norm of the bounded function.
```
theorem finiteMeanState_translation_bound (A : Finset G) (hA : A.Nonempty)
    (g : G) (f : BoundedReal G) :
    |finiteMeanState A (leftPull g f) - finiteMeanState A f| ≤
      boundaryRatio A g * ‖f‖ := by
…
```
Mentions: OAI.PolycyclicRecognition.finiteMeanState

theorem OAI.PolycyclicRecognition.exists_invariantMean_of_folner_net line 57

Source documentation

No countability or finite-generation assumption is required for this compactness step; each group translation has its own vanishing boundary ratio.

theorem exists_invariantMean_of_folner_net
    {ι : Type*} {l : Filter ι} [l.NeBot]
    (A : ι → Finset G) (hA : ∀ i, (A i).Nonempty)
    (hboundary : ∀ g, Tendsto (fun i => boundaryRatio (A i) g) l (𝓝 0)) :
    Nonempty (InvariantMean G) := by
…