SupportSymmetries.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite group of height labels

The segment support determines a finite spanning body in the dual. A linear support isometry preserves that body and hence permutes its vertices. This proves finiteness of the group used to label stationary slopes and profiles.

def OAI.PolycyclicRecognition.heightDualAction line 23
Source documentation
Precomposition of continuous covectors by a height automorphism.
```
def heightDualAction (A : W ≃L[ℝ] W) : (W →L[ℝ] ℝ) ≃L[ℝ] (W →L[ℝ] ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.heightDualAction_apply line 27

theorem OAI.PolycyclicRecognition.supportBody_preserved line 33

Source documentation

A support isometry preserves the concrete dual support body.

theorem supportBody_preserved (A : W ≃L[ℝ] W)
    (hA : ∀ w, D.segmentSupport (A w) = D.segmentSupport w) :
    heightDualAction A '' convexHull ℝ (D.supportForms : Set (W →L[ℝ] ℝ)) =
      convexHull ℝ (D.supportForms : Set (W →L[ℝ] ℝ)) := by
…

Mentions: OAI.PolycyclicRecognition.heightDualAction

theorem OAI.PolycyclicRecognition.finite_support_isometries line 56
Source documentation
There are finitely many possible linear labels. The finite set is determined by the support data, independently of any quasi-isometry.
```
theorem finite_support_isometries :
    Set.Finite {A : W ≃L[ℝ] W | ∀ w, D.segmentSupport (A w) = D.segmentSupport w} := by
…
```
def OAI.PolycyclicRecognition.supportSymmetryGroup line 82
Source documentation
The linear labels form a subgroup, with the concrete finite support isometry condition as membership.
```
def supportSymmetryGroup : Subgroup (W ≃L[ℝ] W) where
…
```
instance OAI.PolycyclicRecognition.finite_supportSymmetryGroup line 94