MautnerMetric.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Fixed vectors from small group sandwiches

These metric arguments are the part of the Mautner phenomenon needed for the actual root-pair calculation. They apply to the continuous isometric action on L². No ergodicity or homogeneous-orbit premise is introduced.

lemma OAI.DukePrimeDegree.dist_sandwich_of_fixed line 26
theorem OAI.DukePrimeDegree.fixed_of_sandwich_tendsto line 37
Source documentation
Large left and right factors which fix the vector may squeeze a small middle factor to a nontrivial group limit. That limit still fixes the vector because both outer factors act isometrically.
```
theorem fixed_of_sandwich_tendsto
    (x : Y) (a b c : ℕ → G) (g : G)
    (ha : ∀ k, a k • x = x) (hb : ∀ k, b k • x = x)
    (hc : Tendsto c atTop (𝓝 1))
    (hlim : Tendsto (fun k => a k * c k * b k) atTop (𝓝 g)) :
    g • x = x := by
…
```
theorem OAI.DukePrimeDegree.fixed_of_conjugate_tendsto line 55
Source documentation
The usual contraction form of Mautner: a group element contracted to identity by elements fixing the vector also fixes the vector.
```
theorem fixed_of_conjugate_tendsto
    (x : Y) (a : ℕ → G) (g : G)
    (ha : ∀ k, a k • x = x)
    (hlim : Tendsto (fun k => a k * g * (a k)⁻¹) atTop (𝓝 1)) :
    g • x = x := by
…
```