HeightHomomorphism.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The corrected height homomorphism

An amenable group acting with bounded height error and finitely many linear height parts has a normal finite-index subgroup with a genuine homomorphism to the height space at bounded distance from the height shifts. In particular the shifts are uniformly bounded on the kernel. The construction combines the exact linear action with an invariant-mean correction.

theorem OAI.PolycyclicRecognition.HeightQuasiAction.exists_correctedHeight line 29
Source documentation
The affine shifts restricted to the linear kernel are at bounded distance from an actual height homomorphism. Amenability is expressed by an invariant mean on all bounded functions on the original group.
```
theorem exists_correctedHeight [FiniteDimensional ℝ W] (Q : HeightQuasiAction H X W) (M : InvariantMean H) :
    ∃ (τ : Q.linearHom.ker →* Multiplicative W) (B : ℝ),
      0 ≤ B ∧ ∀ h, ‖(τ h).toAdd - Q.shift h‖ ≤ B := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightQuasiAction
theorem OAI.PolycyclicRecognition.HeightQuasiAction.shift_bounded_on_kernel line 38
Source documentation
On the kernel of any such correction, the original height shifts are bounded. The kernel is not assumed to be finitely generated.
```
theorem shift_bounded_on_kernel (Q : HeightQuasiAction H X W)
    (τ : Q.linearHom.ker →* Multiplicative W) (B : ℝ)
    (hτ : ∀ h, ‖(τ h).toAdd - Q.shift h‖ ≤ B)
    (h : τ.ker) : ‖Q.shift (h : Q.linearHom.ker)‖ ≤ B := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightQuasiAction

theorem OAI.PolycyclicRecognition.HeightQuasiAction.exists_normal_finiteIndex_height line 50

Source documentation

The finite-index, normal-subgroup and bounded-kernel conclusions of the algebraic part of the recognition argument.

theorem exists_normal_finiteIndex_height [FiniteDimensional ℝ W] (Q : HeightQuasiAction H X W)
    (M : InvariantMean H) (hfinite : Set.Finite (Set.range Q.linear)) :
    ∃ (H₀ : Subgroup H), H₀.Normal ∧ H₀.FiniteIndex ∧
      ∃ (τ : H₀ →* Multiplicative W) (B : ℝ), 0 ≤ B ∧
        (∀ h : H₀, ‖(τ h).toAdd - Q.shift h‖ ≤ B) ∧
        (∀ h : τ.ker, ‖Q.shift (h : H₀)‖ ≤ B) := by
…

Mentions: OAI.PolycyclicRecognition.HeightQuasiAction