PairCoupling.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Translation invariance of the pair coupling

The two commuting translations are written in both product charts. Haar measure times the stationary probability gives the actual invariant coupling.

def OAI.PolycyclicRecognition.pairDomainTranslation line 23
Source documentation
Domain translation, expressed in the target-normalized chart.
```
def pairDomainTranslation (x : G) (q : G × NormalizedPair G Λ) :
    G × NormalizedPair G Λ :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
def OAI.PolycyclicRecognition.pairInverseTargetTranslation line 28
Source documentation
Target translation by y⁻¹, expressed in the source-normalized chart.
```
def pairInverseTargetTranslation (y : G) (q : NormalizedPair G Λ × G) :
    NormalizedPair G Λ × G :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.pairChartTransition_domain line 34
Source documentation
The transition conjugates domain translation to right translation on the second coordinate of the inverse chart.
```
theorem pairChartTransition_domain (x : G) (q : G × NormalizedPair G Λ) :
    pairChartTransition (pairDomainTranslation x q) =
      ((pairChartTransition q).1, (pairChartTransition q).2 * x) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairChartTransition, OAI.PolycyclicRecognition.pairDomainTranslation
theorem OAI.PolycyclicRecognition.pairSourceChart_target line 56
Source documentation
The target action in inverse coordinates is a normalized translation and a left translation depending on the inverse pair.
```
theorem pairSourceChart_target (y : G) (q : NormalizedPair G Λ × G) :
    pairSourceChart (pairInverseTargetTranslation y q) =
      targetTranslate y⁻¹ (pairSourceChart q) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairSourceChart, OAI.PolycyclicRecognition.pairInverseTargetTranslation, OAI.PolycyclicRecognition.targetTranslate
theorem OAI.PolycyclicRecognition.pairTargetChart_target line 73
Source documentation
Target translation in the first chart.
```
theorem pairTargetChart_target (y : G) (q : G × NormalizedPair G Λ) :
    pairTargetChart (y * q.1, q.2) = targetTranslate y (pairTargetChart q) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTargetChart, OAI.PolycyclicRecognition.targetTranslate
theorem OAI.PolycyclicRecognition.pairChartTransition_target line 81
Source documentation
Target translation conjugated through the change of product charts.
```
theorem pairChartTransition_target (y : G) (q : G × NormalizedPair G Λ) :
    pairChartTransition (y⁻¹ * q.1, q.2) =
      pairInverseTargetTranslation y (pairChartTransition q) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairChartTransition, OAI.PolycyclicRecognition.pairInverseTargetTranslation
theorem OAI.PolycyclicRecognition.measurePreserving_pairDomainTranslation line 95
Source documentation
Haar preservation in the target chart follows directly from stationarity and right invariance of Haar measure.
```
theorem measurePreserving_pairDomainTranslation
    (m : Measure G) [SFinite m] [m.IsMulRightInvariant]
    (μ : Measure (NormalizedPair G Λ)) [SFinite μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ] (x : G) :
    MeasurePreserving (pairDomainTranslation x) (m.prod μ) (m.prod μ) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairDomainTranslation
def OAI.PolycyclicRecognition.inversePairCoupling line 117
Source documentation
The coupling measure in inverse coordinates, defined by the actual chart.
```
def inversePairCoupling (m : Measure G) (μ : Measure (NormalizedPair G Λ)) :
    Measure (NormalizedPair G Λ × G) :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.measurePreserving_inversePairCoupling_right line 122

Source documentation

In the inverse chart, the coupling is right invariant in the group fiber.

theorem measurePreserving_inversePairCoupling_right
    (m : Measure G) [SFinite m] [m.IsMulRightInvariant]
    (μ : Measure (NormalizedPair G Λ)) [SFinite μ]
    [SMulInvariantMeasure G (NormalizedPair G Λ) μ] (x : G) :
    MeasurePreserving (fun q : NormalizedPair G Λ × G => (q.1, q.2 * x))
      (inversePairCoupling m μ) (inversePairCoupling m μ) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inversePairCoupling

theorem OAI.PolycyclicRecognition.measurePreserving_inversePairCoupling_target line 143
Source documentation
The same coupling is invariant under the target action in inverse coordinates.
```
theorem measurePreserving_inversePairCoupling_target
    (m : Measure G) [SFinite m] [m.IsMulLeftInvariant]
    (μ : Measure (NormalizedPair G Λ)) [SFinite μ] (y : G) :
    MeasurePreserving (pairInverseTargetTranslation y)
      (inversePairCoupling m μ) (inversePairCoupling m μ) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairInverseTargetTranslation, OAI.PolycyclicRecognition.inversePairCoupling