InvariantMeanGenerators.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

It suffices to make a mean invariant under a generating set

def OAI.PolycyclicRecognition.meanStabilizer line 18
Source documentation
The left translations preserving a linear averaging functional form a subgroup.
```
def meanStabilizer (M : BoundedReal G →ₗ[ℝ] ℝ) : Subgroup G where
…
```

theorem OAI.PolycyclicRecognition.exists_invariantMean_of_approximate_generators line 31

Source documentation

Approximate invariance need only be checked on generators; the limiting functional is invariant under their whole algebraic closure.

theorem exists_invariantMean_of_approximate_generators
    {ι : Type*} {l : Filter ι} [l.NeBot]
    (L : ι → BoundedReal G →ₗ[ℝ] ℝ)
    (hpos : ∀ i f, (∀ g, 0 ≤ f g) → 0 ≤ L i f)
    (hone : ∀ i, L i 1 = 1) (S : Set G) (hS : Subgroup.closure S = ⊤)
    (hdefect : ∀ g ∈ S, ∀ f, Tendsto (fun i => L i (leftPull g f) - L i f) l (𝓝 0)) :
    Nonempty (InvariantMean G) := by
…