ExtensionInvariantMean.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Invariant means on extensions

Average first on each kernel coset and then on the quotient. All averages act on the actual bounded real functions used in the height correction.

def OAI.PolycyclicRecognition.boundedFunctionPull line 21
theorem OAI.PolycyclicRecognition.boundedFunctionPull_apply line 29
theorem OAI.PolycyclicRecognition.boundedFunctionPull_one line 33
theorem OAI.PolycyclicRecognition.boundedFunctionPull_norm_le line 36
def OAI.PolycyclicRecognition.imageInvariantMean line 44
Source documentation
An invariant mean descends along a surjective group homomorphism.
```
def imageInvariantMean (φ : G →* Q) (hφ : Function.Surjective φ)
    (M : InvariantMean G) : InvariantMean Q where
…
```
def OAI.PolycyclicRecognition.kernelSlice line 62
def OAI.PolycyclicRecognition.kernelAverage line 66
theorem OAI.PolycyclicRecognition.kernelAverage_one line 83

theorem OAI.PolycyclicRecognition.kernelAverage_leftPull line 93

Source documentation

Changing a representative inserts a kernel translation, which disappears under the inner mean.

theorem kernelAverage_leftPull (φ : G →* Q) (s : Q → G) (hs : ∀ q, φ (s q) = q)
    (M : InvariantMean φ.ker) (g : G) (f : BoundedReal G) :
    kernelAverage φ s M (leftPull g f) = leftPull (φ g) (kernelAverage φ s M f) := by
…

Mentions: OAI.PolycyclicRecognition.kernelAverage

def OAI.PolycyclicRecognition.extensionInvariantMean line 112
theorem OAI.PolycyclicRecognition.invariantMean_of_extension line 124
def OAI.PolycyclicRecognition.finiteInvariantMean line 131
Source documentation
The normalized counting mean on a finite group.
```
def finiteInvariantMean [Finite G] : InvariantMean G := by
…
```
theorem OAI.PolycyclicRecognition.invariantMean_of_normal_subgroup line 142
theorem OAI.PolycyclicRecognition.invariantMean_of_finiteIndex line 152
Source documentation
No normality assumption is needed for a finite extension: restrict to the normal core, then average over its finite quotient.
```
theorem invariantMean_of_finiteIndex (K : Subgroup G) [K.FiniteIndex]
    (hK : Nonempty (InvariantMean K)) : Nonempty (InvariantMean G) := by
…
```