HilbertOrbitAverage.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Hilbert averaging over a group orbit

The closed convex hull of a unitary orbit has a fixed vector of minimal norm. This requires no invariant mean on the acting group. It supplies the averaging step in the construction of ergodic conditional component measures.

def OAI.PolycyclicRecognition.hilbertOrbitHull line 26
Source documentation
The closed convex hull of the actual orbit.
```
def hilbertOrbitHull : Set E := closure (convexHull ℝ (range (fun g => ρ g x)))
```
theorem OAI.PolycyclicRecognition.hilbertOrbitHull_nonempty line 28
theorem OAI.PolycyclicRecognition.hilbertOrbitHull_convex line 31
theorem OAI.PolycyclicRecognition.hilbertOrbitHull_map line 35
Source documentation
Every acting isometry preserves the closed convex hull.
```
theorem hilbertOrbitHull_map (g : G) {y : E} (hy : y ∈ hilbertOrbitHull ρ x) :
    ρ g y ∈ hilbertOrbitHull ρ x := by
…
```
Mentions: OAI.PolycyclicRecognition.hilbertOrbitHull
theorem OAI.PolycyclicRecognition.exists_fixed_in_hilbertOrbitHull line 52
Source documentation
A fixed vector is a norm limit of finite convex combinations of the orbit.
```
theorem exists_fixed_in_hilbertOrbitHull :
    ∃ y ∈ hilbertOrbitHull ρ x, ∀ g : G, ρ g y = y := by
…
```
Mentions: OAI.PolycyclicRecognition.hilbertOrbitHull
def OAI.PolycyclicRecognition.isometricLinearAction line 78
Source documentation
The bundled unitary representation of a real linear isometric action.
```
def isometricLinearAction : G →* (E ≃ₗᵢ[ℝ] E) where
…
```
theorem OAI.PolycyclicRecognition.exists_fixed_in_convex_orbit line 89
Source documentation
The convex orbit averaging theorem in the unbundled action notation.
```
theorem exists_fixed_in_convex_orbit (x : E) :
    ∃ y ∈ closure (convexHull ℝ (range (fun g : G => g • x))),
      ∀ g : G, g • y = y :=
…
```