CouplingTransfer.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Transfer functions in the two coupling charts

The transfer is lifted by adding target height. Its domain defect is the original stationary cocycle defect. In inverse coordinates, differences inside a fiber are the same defects, and fiber averaging gives the exact inverse transfer identity.

def OAI.PolycyclicRecognition.pairTransferLift line 27
Source documentation
Extend a section transfer by target-height equivariance.
```
def pairTransferLift (π : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (q : G × NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
def OAI.PolycyclicRecognition.pairTransferDefect line 32
Source documentation
The stationary domain defect, with the proposed mean height subtracted.
```
def pairTransferDefect (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (t : G) (p : NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
def OAI.PolycyclicRecognition.inverseFiberTransfer line 37
Source documentation
In inverse coordinates, subtract the proposed domain height.
```
def inverseFiberTransfer (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (q : NormalizedPair G Λ × G) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
theorem OAI.PolycyclicRecognition.pairTransferLift_domain line 42
theorem OAI.PolycyclicRecognition.pairChartTransition_symm_domain line 52
Source documentation
The inverse chart intertwines domain translation with right translation inside each fiber.
```
theorem pairChartTransition_symm_domain (t : G) (q : NormalizedPair G Λ × G) :
    pairDomainTranslation t (pairChartTransition.symm q) =
      pairChartTransition.symm (q.1, q.2 * t) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairDomainTranslation

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_sub line 60

Source documentation

Differences of two fiber values are original cocycle defects.

theorem inverseFiberTransfer_sub (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (p : NormalizedPair G Λ) (x₁ x₂ : G) :
    inverseFiberTransfer π l φ (p, x₁) - inverseFiberTransfer π l φ (p, x₂) =
      pairTransferDefect π l φ (x₂⁻¹ * x₁)
        (pairChartTransition.symm (p, x₂)).2 := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inverseFiberTransfer, OAI.PolycyclicRecognition.pairTransferDefect

theorem OAI.PolycyclicRecognition.pairChartTransition_symm_target line 74
Source documentation
Target translation in the inverse chart, expressed back in target coordinates.
```
theorem pairChartTransition_symm_target (y : G) (q : NormalizedPair G Λ × G) :
    pairChartTransition.symm (pairInverseTargetTranslation y q) =
      (y⁻¹ * (pairChartTransition.symm q).1, (pairChartTransition.symm q).2) := by
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairInverseTargetTranslation

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_target line 82

Source documentation

The pointwise target transfer identity before averaging.

theorem inverseFiberTransfer_target (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (y : G) (q : NormalizedPair G Λ × G) :
    inverseFiberTransfer π l φ (pairInverseTargetTranslation y q) =
      inverseFiberTransfer π l φ q - (π y).toAdd + (l (q.1.val.1 y)).toAdd := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inverseFiberTransfer, OAI.PolycyclicRecognition.pairInverseTargetTranslation

theorem OAI.PolycyclicRecognition.inverseFiberTransfer_normalizedTranslate line 93

Source documentation

A version with a fixed integration coordinate, suitable for averaging.

theorem inverseFiberTransfer_normalizedTranslate (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (y : G) (p : NormalizedPair G Λ) (x : G) :
    inverseFiberTransfer π l φ (normalizedTranslate y p, x) =
      inverseFiberTransfer π l φ (p, p.val.1 y * x) -
        (π y).toAdd + (l (p.val.1 y)).toAdd := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inverseFiberTransfer, OAI.PolycyclicRecognition.normalizedTranslate

def OAI.PolycyclicRecognition.inverseAveragedTransfer line 104
Source documentation
Average the transfer over a whole probability fiber.
```
def inverseAveragedTransfer (β : Measure G) (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (p : NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair
def OAI.PolycyclicRecognition.inverseAverageError line 109
Source documentation
The error is the average of differences inside one fiber.
```
def inverseAverageError (β : Measure G) (π l : G →* Multiplicative W)
    (φ : NormalizedPair G Λ → W) (y : G) (p : NormalizedPair G Λ) : W :=
…
```
Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.inverseAveragedTransfer_identity line 116

Source documentation

Averaging yields the exact inverse-transfer identity; integrability is required only on the two regions actually being averaged.

theorem inverseAveragedTransfer_identity (β : Measure G) [IsProbabilityMeasure β]
    (π l : G →* Multiplicative W) (φ : NormalizedPair G Λ → W)
    (y : G) (p : NormalizedPair G Λ)
    (h₁ : Integrable (fun x => inverseFiberTransfer π l φ (p, p.val.1 y * x)) β)
    (h₂ : Integrable (fun x => inverseFiberTransfer π l φ (p, x)) β) :
    inverseAveragedTransfer β π l φ (normalizedTranslate y p) -
      inverseAveragedTransfer β π l φ p =
      -(π y).toAdd + (l (p.val.1 y)).toAdd + inverseAverageError β π l φ y p := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.inverseFiberTransfer, OAI.PolycyclicRecognition.inverseAveragedTransfer, OAI.PolycyclicRecognition.normalizedTranslate, OAI.PolycyclicRecognition.inverseAverageError