InvariantFactorComponents.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Invariance of the conditional component measures

Only countably many identities are intersected. Continuity of the action extends invariance from the dense sequence to the full acting group.

theorem OAI.PolycyclicRecognition.factorConditionalKernel_invariant_ae_dense line 27

Source documentation

The invariant factor may have a sigma algebra that is not countably generated.

theorem factorConditionalKernel_invariant_ae_dense
    (hfi : ∀ (g : G) (s : Set Y), MeasurableSet s →
      ∀ x, f (g • x) ∈ s ↔ f x ∈ s) :
    ∀ᵐ y ∂μ.map f, SMulInvariantMeasure G X (factorConditionalKernel μ f hf y) := by
…

Mentions: OAI.PolycyclicRecognition.factorConditionalKernel

theorem OAI.PolycyclicRecognition.invariantConditionalMeasures_invariant_ae line 39
Source documentation
Almost every component of conditioning on all invariant sets is invariant.
```
theorem invariantConditionalMeasures_invariant_ae :
    ∀ᵐ x ∂μ, SMulInvariantMeasure G X (invariantConditionalMeasures (G := G) μ x) := by
…
```
Mentions: OAI.PolycyclicRecognition.invariantConditionalMeasures