InvariantFactor.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Conditioning on all invariant measurable sets

The factor retains the original points but equips them with the sigma algebra of invariant sets. Its conditional kernel is pointwise constant on every orbit and has the original probability as its barycenter.

def OAI.PolycyclicRecognition.invariantSigma line 23
Source documentation
The sigma algebra of measurable sets invariant under the entire action.
```
def invariantSigma : MeasurableSpace X :=
…
```
theorem OAI.PolycyclicRecognition.measurableSet_invariantSigma line 26
theorem OAI.PolycyclicRecognition.invariantSigma_le line 34
structure OAI.PolycyclicRecognition.InvariantFactor line 38
Source documentation
The measurable factor, without imposing any quotient topology.
```
structure InvariantFactor (G X : Type*) where
…
```
instance OAI.PolycyclicRecognition.(instance at line 41) line 41
def OAI.PolycyclicRecognition.invariantFactorMap line 45
Source documentation
Identity on points, with the coarser invariant sigma algebra as codomain.
```
def invariantFactorMap (x : X) : InvariantFactor G X := ⟨x⟩
```
Mentions: OAI.PolycyclicRecognition.InvariantFactor
theorem OAI.PolycyclicRecognition.measurable_invariantFactorMap line 47

theorem OAI.PolycyclicRecognition.invariantFactor_observable line 58

Source documentation

Every measurable scalar observable on the factor is exactly orbit invariant.

theorem invariantFactor_observable {Z : Type*} [MeasurableSpace Z]
    [MeasurableSingletonClass Z] (f : InvariantFactor G X → Z) (hf : Measurable f)
    (g : G) (x : X) : f (invariantFactorMap G X (g • x)) =
      f (invariantFactorMap G X x) := by
…

Mentions: OAI.PolycyclicRecognition.InvariantFactor, OAI.PolycyclicRecognition.invariantFactorMap

def OAI.PolycyclicRecognition.invariantConditionalKernel line 78
Source documentation
Conditional probabilities over the complete invariant sigma algebra.
```
def invariantConditionalKernel : Kernel (InvariantFactor G X) X :=
…
```
Mentions: OAI.PolycyclicRecognition.InvariantFactor
instance OAI.PolycyclicRecognition.invariantConditionalKernel_markov line 81
def OAI.PolycyclicRecognition.invariantConditionalMeasures line 86
Source documentation
Pull the conditional kernel back to the original space.
```
def invariantConditionalMeasures (x : X) : Measure X :=
…
```
theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_probability line 89
theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_measurable line 94
theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_smul line 97
theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_barycenter line 103