MeanSubgroup.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Restricting invariant means to subgroups

The finite-index height kernel in the recognition argument inherits amenability from the ambient group. The construction below works for an arbitrary subgroup: choose representatives for right cosets, construct an equivariant map to the subgroup, and extend each bounded function by composition with this map.

def OAI.PolycyclicRecognition.rightCosetRepresentative line 27
Source documentation
The representative selected for the right coset containing g.
```
def rightCosetRepresentative (K : Subgroup G) (g : G) : G :=
…
```
def OAI.PolycyclicRecognition.subgroupCoordinate line 31
Source documentation
A right-coset transversal gives an equivariant coordinate in the subgroup.
```
def subgroupCoordinate (K : Subgroup G) (g : G) : K :=
…
```
theorem OAI.PolycyclicRecognition.subgroupCoordinate_mul line 38
Source documentation
The subgroup coordinate intertwines the left action of the subgroup.
```
theorem subgroupCoordinate_mul (K : Subgroup G) (k : K) (g : G) :
    subgroupCoordinate K ((k : G) * g) = k * subgroupCoordinate K g := by
…
```
Mentions: OAI.PolycyclicRecognition.subgroupCoordinate
def OAI.PolycyclicRecognition.subgroupFunctionExtension line 52
Source documentation
Extend a bounded subgroup function to the whole group by the equivariant coordinate.
```
def subgroupFunctionExtension (K : Subgroup G) : BoundedReal K →ₗ[ℝ] BoundedReal G where
…
```
theorem OAI.PolycyclicRecognition.subgroupFunctionExtension_apply line 66
theorem OAI.PolycyclicRecognition.subgroupFunctionExtension_one line 70
theorem OAI.PolycyclicRecognition.subgroupFunctionExtension_leftPull line 77
Source documentation
Equivariance makes extension commute with pullback by subgroup translations.
```
theorem subgroupFunctionExtension_leftPull (K : Subgroup G) (k : K) (f : BoundedReal K) :
    subgroupFunctionExtension K (leftPull k f) =
      leftPull (k : G) (subgroupFunctionExtension K f) := by
…
```
Mentions: OAI.PolycyclicRecognition.subgroupFunctionExtension
def OAI.PolycyclicRecognition.subgroupInvariantMean line 86
Source documentation
Every subgroup of a group with an invariant mean has an invariant mean.
```
def subgroupInvariantMean (M : InvariantMean G) (K : Subgroup G) : InvariantMean K where
…
```