StationaryProbability.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Invariant probability on a compact space of maps

The orbit average of an actual invariant mean is a positive functional on compactly supported continuous functions. Its Riesz measure is a regular probability and is invariant under the given action. No invariant measure is postulated in this construction.

def OAI.PolycyclicRecognition.boundedOrbit line 29
Source documentation
Restrict a bounded continuous function to an orbit, as an actual bounded function on the acting group.
```
def boundedOrbit (x : X) (f : C_c(X, ℝ)) : BoundedReal G :=
…
```
theorem OAI.PolycyclicRecognition.boundedOrbit_apply line 34
def OAI.PolycyclicRecognition.orbitAverage line 38
Source documentation
The positive orbit-average functional.
```
def orbitAverage (M : InvariantMean G) (x : X) : C_c(X, ℝ) →ₚ[ℝ] ℝ where
…
```
def OAI.PolycyclicRecognition.orbitProbability line 54
Source documentation
The regular Riesz measure associated with the invariant orbit average.
```
def orbitProbability (M : InvariantMean G) (x : X) : Measure X :=
…
```
instance OAI.PolycyclicRecognition.orbitProbability_regular line 57
instance OAI.PolycyclicRecognition.orbitProbability_finite line 61
theorem OAI.PolycyclicRecognition.integral_orbitProbability line 65
instance OAI.PolycyclicRecognition.orbitProbability_probability line 70
theorem OAI.PolycyclicRecognition.orbitProbability_map_smul line 83
Source documentation
Every group element preserves the orbit-average probability.
```
theorem orbitProbability_map_smul (M : InvariantMean G) (x : X) (g : G) :
    Measure.map (g • ·) (orbitProbability M x) = orbitProbability M x := by
…
```
Mentions: OAI.PolycyclicRecognition.orbitProbability
instance OAI.PolycyclicRecognition.orbitProbability_invariant line 106
theorem OAI.PolycyclicRecognition.exists_invariant_probability line 114
Source documentation
Amenability supplies a regular invariant probability on every nonempty compact Hausdorff action space.
```
theorem exists_invariant_probability (M : InvariantMean G) [Nonempty X] :
    ∃ μ : Measure X, μ.Regular ∧ IsProbabilityMeasure μ ∧ SMulInvariantMeasure G X μ := by
…
```