FiniteInvariantOrbit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Selecting a label in a finite linear group

Embedding a vector in the Euclidean product of all its group translates provides an invariant strictly convex norm without changing the topology or norm instances on the original height space.

def OAI.PolycyclicRecognition.finiteOrbitEmbedding line 25
Source documentation
All group translates, recorded in a finite Euclidean product.
```
def finiteOrbitEmbedding : W →ₗ[ℝ] PiLp 2 (fun _ : Γ => E) :=
…
```
theorem OAI.PolycyclicRecognition.finiteOrbitEmbedding_apply line 30
theorem OAI.PolycyclicRecognition.finiteOrbitEmbedding_injective line 34
theorem OAI.PolycyclicRecognition.finiteOrbitEmbedding_norm line 41

theorem OAI.PolycyclicRecognition.exists_eq_label_of_finite_group_convex_orbit line 50

Source documentation

A member of a finite linear group lying pointwise in the convex orbit of a finite family is one of the members of that family.

theorem exists_eq_label_of_finite_group_convex_orbit
    {J : Type*} [Finite J] (he : Function.Injective e)
    (B : Γ) (A : J → Γ)
    (hconv : ∀ w, B.val w ∈ convexHull ℝ (range fun j => (A j).val w)) :
    ∃ j, B = A j := by
…