AffineAction.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact linear parts of a uniformly affine height quasi-action

A bounded error on a surjective real height quotient forces the linear parts of a quasi-action to multiply exactly. This is the algebraic argument in Proposition prop:recognition-from-height of Quasi-isometric recognition of virtually polycyclic groups, Section 11.

theorem OAI.PolycyclicRecognition.linear_eq_zero_of_uniform_bound line 23
Source documentation
A real linear map that is uniformly bounded on its entire domain vanishes.
```
theorem linear_eq_zero_of_uniform_bound (L : W →L[ℝ] W)
    (C : ℝ) (hC : ∀ w, ‖L w‖ ≤ C) : L = 0 := by
…
```
theorem OAI.PolycyclicRecognition.linear_parts_eq_of_bounded_affine_difference line 37
Source documentation
Two affine maps a bounded distance apart have identical linear parts.
```
theorem linear_parts_eq_of_bounded_affine_difference
    (L M : W →L[ℝ] W) (b : W) (C : ℝ)
    (h : ∀ w, ‖b + L w - M w‖ ≤ C) : L = M := by
…
```
structure OAI.PolycyclicRecognition.HeightQuasiAction line 51
Source documentation
Height-coordinate data for a quasi-action. All geometric estimates are recorded explicitly, and no exact action law for F is assumed.
```
structure HeightQuasiAction (H X W : Type*) [Group H]
    [NormedAddCommGroup W] [NormedSpace ℝ W] where
…
```

theorem OAI.PolycyclicRecognition.HeightQuasiAction.affine_composition_bound line 73

Source documentation

The composition defect of the affine approximations has a bound independent of the height argument. The bound may depend on the first linear map.

theorem affine_composition_bound (h k : H) (x : X) :
    ‖(Q.shift h + Q.linear h (Q.shift k) - Q.shift (h * k)) +
      Q.linear h (Q.linear k (Q.height x)) - Q.linear (h * k) (Q.height x)‖ ≤
      Q.error + ‖(Q.linear h).toContinuousLinearMap‖ * Q.error +
        Q.composition_error + Q.error := by
…

theorem OAI.PolycyclicRecognition.HeightQuasiAction.linear_mul line 120
Source documentation
Bounded quasi-action errors force the linear parts to compose exactly.
```
theorem linear_mul (h k : H) : Q.linear (h * k) = Q.linear h * Q.linear k := by
…
```
def OAI.PolycyclicRecognition.HeightQuasiAction.linearHom line 134
Source documentation
The exact homomorphism of linear height parts.
```
def linearHom : H →* W ≃L[ℝ] W :=
…
```
theorem OAI.PolycyclicRecognition.HeightQuasiAction.linearHom_apply line 138
theorem OAI.PolycyclicRecognition.HeightQuasiAction.finiteIndex_linear_kernel line 142
Source documentation
When only finitely many linear parts occur, the subgroup with trivial linear part has finite index, as required in the recognition argument.
```
theorem finiteIndex_linear_kernel (hfinite : Set.Finite (Set.range Q.linear)) :
    Q.linearHom.ker.FiniteIndex := by
…
```
def OAI.PolycyclicRecognition.HeightQuasiAction.translationDefect line 149
Source documentation
Uniform defect bound for translations on the kernel of the linear action.
```
def translationDefect : ℝ :=
…
```
theorem OAI.PolycyclicRecognition.HeightQuasiAction.translation_defect_le line 154
Source documentation
Restricting the height shifts to the subgroup with trivial linear part gives an additive map up to a uniformly bounded error.
```
theorem translation_defect_le (h k : Q.linearHom.ker) :
    ‖Q.shift (h * k) - Q.shift h - Q.shift k‖ ≤ Q.translationDefect := by
…
```