PairOrbit.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

+# Compact invariant orbit closures of individual pairs

The stationary construction can be performed inside the orbit closure of the given quasi-isometry pair, rather than on an unrelated part of the full pair space. The orbit closure carries the restricted continuous action.

def OAI.PolycyclicRecognition.PairOrbit line 24
Source documentation
The actual orbit closure of a normalized quasi-isometry pair.
```
def PairOrbit (p : NormalizedPair G Λ) := closure (MulAction.orbit G p)
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
instance OAI.PolycyclicRecognition.(instance at line 26) line 26
instance OAI.PolycyclicRecognition.(instance at line 29) line 29
instance OAI.PolycyclicRecognition.pairOrbitAction line 32
theorem OAI.PolycyclicRecognition.pairOrbit_smul_val line 38
instance OAI.PolycyclicRecognition.pairOrbitContinuousAction line 41
instance OAI.PolycyclicRecognition.pairOrbit_polishSpace line 46
theorem OAI.PolycyclicRecognition.exists_pairOrbit_ergodic_probability line 51
Source documentation
A stationary measure supported on the orbit closure of the chosen pair. Both amenability and the decomposition input are used at that precise space.
```
theorem exists_pairOrbit_ergodic_probability [SecondCountableTopology G]
    (p : NormalizedPair G Λ) [MeasurableSpace (PairOrbit p)] [BorelSpace (PairOrbit p)]
    (M : ThompsonNonamenability.InvariantMean G)
    (hdec : ErgodicDecompositionInput G (PairOrbit p)) :
    ∃ μ : Measure (PairOrbit p),
      IsProbabilityMeasure μ ∧ ErgodicSMul G (PairOrbit p) μ :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.PairOrbit, OAI.ThompsonNonamenability.InvariantMean, OAI.PolycyclicRecognition.ErgodicDecompositionInput

theorem OAI.PolycyclicRecognition.pairOrbit_pushforward_ergodic line 61

Source documentation

Push the orbit measure to the full pair space. The measure remains ergodic, so it admits the height cocycle.

theorem pairOrbit_pushforward_ergodic (p : NormalizedPair G Λ)
    [MeasurableSpace (PairOrbit p)] [BorelSpace (PairOrbit p)]
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    (μ : Measure (PairOrbit p)) [ErgodicSMul G (PairOrbit p) μ] :
    ErgodicSMul G (NormalizedPair G Λ) (μ.map Subtype.val) :=
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.PairOrbit