FiniteOrbitAverage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite convex averages of translates

The same finite data act on actual functions and on their L2 classes. This allows the averages to be transported to a conditional component measure.

structure OAI.PolycyclicRecognition.FiniteOrbitAverage line 19
Source documentation
A finite probability distribution on acting elements.
```
structure FiniteOrbitAverage (G : Type*) where
…
```
def OAI.PolycyclicRecognition.FiniteOrbitAverage.apply line 32
Source documentation
The actual finite average, with the inverse convention of the Koopman action.
```
def FiniteOrbitAverage.apply (A : FiniteOrbitAverage G) (f : X → ℝ) (x : X) : ℝ :=
…
```
Mentions: OAI.PolycyclicRecognition.FiniteOrbitAverage
theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.apply_nonneg line 35
theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.apply_le_one line 39
theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.measurable_apply line 48
def OAI.PolycyclicRecognition.FiniteOrbitAverage.onL2 line 57
Source documentation
The same average of the actual unitary operators.
```
def FiniteOrbitAverage.onL2 (A : FiniteOrbitAverage G) (v : Lp ℝ 2 μ) : Lp ℝ 2 μ :=
…
```
Mentions: OAI.PolycyclicRecognition.FiniteOrbitAverage
theorem OAI.PolycyclicRecognition.exists_finiteOrbitAverage line 61
Source documentation
Every vector in the convex hull of an orbit has finite averaging data.
```
theorem exists_finiteOrbitAverage (v w : Lp ℝ 2 μ)
    (hw : w ∈ convexHull ℝ (range (fun g : G => stationaryPullback μ g v))) :
    ∃ A : FiniteOrbitAverage G, A.onL2 μ v = w := by
…
```
Mentions: OAI.PolycyclicRecognition.stationaryPullback, OAI.PolycyclicRecognition.FiniteOrbitAverage
theorem OAI.PolycyclicRecognition.FiniteOrbitAverage.onL2_coe line 79
Source documentation
Pointwise representatives of the finite Hilbert average.
```
theorem FiniteOrbitAverage.onL2_coe (A : FiniteOrbitAverage G) (v : Lp ℝ 2 μ) :
    (A.onL2 μ v : X → ℝ) =ᵐ[μ] A.apply v := by
…
```
Mentions: OAI.PolycyclicRecognition.FiniteOrbitAverage