PairAction.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

+# The normalized translation action on pairs

For a pair (F,B), normalization of domain translation by x has forward map F(x)⁻¹ F(xz) and inverse map x⁻¹ B(F(x)z). These are actual maps, with all Lipschitz and quasi-inverse bounds retained. Inverting the parameter converts the manuscript's right action into a left action.

def OAI.PolycyclicRecognition.translatePair line 27
Source documentation
Normalize domain translation, on pairs of continuous maps.
```
def translatePair (x : G) (p : C(G, G) × C(G, G)) : C(G, G) × C(G, G) :=
…
```
theorem OAI.PolycyclicRecognition.translatePair_bounds_of_bounds line 34
theorem OAI.PolycyclicRecognition.translatePair_bounds line 73
def OAI.PolycyclicRecognition.normalizePair line 78
Source documentation
Every pair satisfying the actual coarse bounds has a normalized representative.
```
def normalizePair {Λ : ℝ≥0} (p : C(G, G) × C(G, G))
    (hp : LipschitzPairBounds G Λ p) : NormalizedPair G Λ :=
…
```
Mentions: OAI.PolycyclicRecognition.LipschitzPairBounds, OAI.PolycyclicRecognition.NormalizedPair
def OAI.PolycyclicRecognition.normalizedTranslate line 83
Source documentation
Translation as a map of the compact normalized section.
```
def normalizedTranslate {Λ : ℝ≥0} (x : G) (p : NormalizedPair G Λ) :
    NormalizedPair G Λ := ⟨translatePair x p.val, translatePair_bounds Λ p x⟩
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.translatePair, OAI.PolycyclicRecognition.translatePair_bounds
theorem OAI.PolycyclicRecognition.normalizedTranslate_one line 87
theorem OAI.PolycyclicRecognition.normalizedTranslate_mul line 97
instance OAI.PolycyclicRecognition.normalizedPairAction line 104
Source documentation
The left action corresponding to normalized right translation.
```
instance normalizedPairAction (Λ : ℝ≥0) : MulAction G (NormalizedPair G Λ) where
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.normalizedPair_smul_fst line 115
theorem OAI.PolycyclicRecognition.normalizedPair_smul_snd line 120
theorem OAI.PolycyclicRecognition.continuous_translatePair line 127
instance OAI.PolycyclicRecognition.normalizedPairContinuousAction line 139

theorem OAI.PolycyclicRecognition.exists_normalizedPair_probability line 148

Source documentation

The construction of the stationary probability applies to the actual normalized pair action.

theorem exists_normalizedPair_probability (Λ : ℝ≥0)
    [Nonempty (NormalizedPair G Λ)]
    [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
    (M : ThompsonNonamenability.InvariantMean G) :
    ∃ μ : MeasureTheory.Measure (NormalizedPair G Λ),
      μ.Regular ∧ MeasureTheory.IsProbabilityMeasure μ ∧
        SMulInvariantMeasure G (NormalizedPair G Λ) μ := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.ThompsonNonamenability.InvariantMean