DenseInvariantMeasure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Invariance on a dense set of acting elements

For a continuous action on a compact metric space, a finite measure invariant under a dense family of group elements is invariant under the whole group. This turns countably many almost-everywhere identities of conditional kernels into invariance of their components for a locally compact second countable group.

theorem OAI.PolycyclicRecognition.smulInvariantMeasure_of_denseRange line 30
Source documentation
Dense invariance is sufficient; the dense family need not be a subgroup.
```
theorem smulInvariantMeasure_of_denseRange (a : ι → G) (ha : DenseRange a)
    (hν : ∀ i, ν.map (a i • ·) = ν) : SMulInvariantMeasure G X ν := by
…
```