ConvexOrbit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From convex orbit constraints to a single linear label

theorem OAI.PolycyclicRecognition.mem_of_mem_convexHull_of_norm_eq line 15
Source documentation
Strict convexity prevents a convex combination of points in a closed ball from lying on the sphere unless it is one of the original points. This is the finite-orbit selection step of the profile affinity argument.
```
theorem mem_of_mem_convexHull_of_norm_eq
    {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W] [StrictConvexSpace ℝ W]
    {s : Set W} {x : W} {r : ℝ}
    (hs : ∀ y ∈ s, ‖y‖ ≤ r) (hx : x ∈ convexHull ℝ s) (hnorm : ‖x‖ = r) :
    x ∈ s := by
…
```

theorem OAI.PolycyclicRecognition.exists_eq_of_convex_orbit line 39

Source documentation

A linear map lying pointwise in a finite orbit convex hull is one of the orbit maps if all these vectors have the same strictly convex norm.

theorem exists_eq_of_convex_orbit
    {ι : Type u} [Finite ι] {W : Type v}
    [NormedAddCommGroup W] [NormedSpace ℝ W] [StrictConvexSpace ℝ W]
    (B : W →ₗ[ℝ] W) (A : ι → W →ₗ[ℝ] W)
    (hconv : ∀ w, B w ∈ convexHull ℝ (Set.range fun i => A i w))
    (hnorm : ∀ w i, ‖A i w‖ = ‖B w‖) : ∃ i, B = A i := by
…