PairCharts.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

+# The two product charts of the space of quasi-inverse pairs

Target normalization gives G × X; inverse normalization gives X × G, where the latter copy of X represents inverse maps. Their transition is an actual homeomorphism. This is the geometric coordinate change used for the inverse-coupling measure, before any disintegration or fiber averaging.

abbrev OAI.PolycyclicRecognition.CoarsePair line 23
Source documentation
All pairs with the fixed coarse bounds, without basepoint normalization.
```
abbrev CoarsePair (G : Type*) [MetricSpace G] (Λ : ℝ≥0) :=
…
```
def OAI.PolycyclicRecognition.targetTranslatePair line 26
theorem OAI.PolycyclicRecognition.targetTranslatePair_bounds line 31
def OAI.PolycyclicRecognition.targetTranslate line 57
theorem OAI.PolycyclicRecognition.continuous_targetTranslatePair line 61
def OAI.PolycyclicRecognition.swapCoarsePair line 74
Source documentation
Swapping the two maps preserves all six bounds.
```
def swapCoarsePair : CoarsePair G Λ ≃ₜ CoarsePair G Λ where
…
```
Mentions: OAI.PolycyclicRecognition.CoarsePair
def OAI.PolycyclicRecognition.pairTargetChart line 85
Source documentation
The first global product chart is target translation of a normalized pair.
```
def pairTargetChart : (G × NormalizedPair G Λ) ≃ₜ CoarsePair G Λ where
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.CoarsePair
def OAI.PolycyclicRecognition.pairSourceChart line 111
Source documentation
The second product chart parametrizes inverse-normalized pairs. It is obtained by swapping maps, with the inverse on the group coordinate.
```
def pairSourceChart : (NormalizedPair G Λ × G) ≃ₜ CoarsePair G Λ :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.CoarsePair
def OAI.PolycyclicRecognition.pairChartTransition line 117
Source documentation
The exact coordinate change underlying the inverse coupling.
```
def pairChartTransition : (G × NormalizedPair G Λ) ≃ₜ (NormalizedPair G Λ × G) :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.pairSourceChart_forward line 120
theorem OAI.PolycyclicRecognition.pairSourceChart_inverse line 125
theorem OAI.PolycyclicRecognition.pairChartTransition_group line 128
theorem OAI.PolycyclicRecognition.pairChartTransition_forward line 133
theorem OAI.PolycyclicRecognition.pairChartTransition_inverse line 139