CartanTiledSourceCell.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The counted samplers on the original quotient/kernel probability cell

def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceQuotientCoordinates line 47
Source documentation
The actual quotient chart associated to the section retained by the tiles.
```
def TiledProbeChainData.sourceQuotientCoordinates :
    (Fin (finrank ℝ (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)) → ℝ) ≃ₜ Q.carrier :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection line 52
Source documentation
The tile construction's fixed linear section as a continuous group section.
```
def TiledProbeChainData.sourceSection : C(Q.carrier, F.N.carrier) :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection_coordinates line 58
Source documentation
The fixed section evaluated in the actual quotient chart.
```
theorem TiledProbeChainData.sourceSection_coordinates
    (hchartN : ∀ v, chartN v = F.ExpN v)
    (z : Fin (finrank ℝ (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)) → ℝ) :
    TiledProbeChainData.sourceSection (T := T) (M := M) (F := F) (hunimod := hunimod) (eW := eW) (C := C)
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection
def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceQuotientCell line 76
Source documentation
The fixed quotient part of the original source probability cell.
```
def TiledProbeChainData.sourceQuotientCell : Set Q.carrier :=
…
```
def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceKernelCell line 85
Source documentation
The scale-dependent kernel part of the original source cell.
```
def TiledProbeChainData.sourceKernelCell (n : ℕ) : Set πQ.ker :=
…
```
def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceCell line 91
Source documentation
The original quotient and kernel cell underlying the tile probes.
```
def TiledProbeChainData.sourceCell (n : ℕ) : Set (Q.carrier × πQ.ker) :=
…
```
def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceCoordinates line 104
Source documentation
Reparametrization uses the actual Haar product cell, so the selected probability measure can be chosen there before concentration is applied.
```
def TiledProbeChainData.sourceCoordinates (n : ℕ) :=
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection_rightInverse line 117

Source documentation

This section is a right inverse of the actual source quotient.

theorem TiledProbeChainData.sourceSection_rightInverse
    (hπ : ∀ v, πQ (chartN (F.N.equiv v)) =
      chartQ (Q.equiv ((M.coneWordIdeal C).toSubmodule.mkQ v))) :
    ∀ q, πQ (TiledProbeChainData.sourceSection (T := T) (M := M) (F := F) (hunimod := hunimod) (eW := eW) (C := C)
…

Mentions: OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceSection

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.source_first line 129
Source documentation
The first sampled endpoint is exactly kernel times the fixed section, with no change to the original sampling measure or chosen starting point.
```
theorem TiledProbeChainData.source_first
    (hchartN : ∀ v, chartN v = F.ExpN v) (n : ℕ)
    (y : (TiledProbeChainData.sourceCell (T := T) (M := M) (F := F) (hunimod := hunimod) (eW := eW) (C := C)
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceCell
theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.source_chains line 170
Source documentation
Every stored chain is retained on the original source probability cell.
```
theorem TiledProbeChainData.source_chains :
    let ψ := fun n => TiledProbeChainData.sourceCoordinates (T := T) (M := M) (F := F) (hunimod := hunimod) (eW := eW) (C := C)
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceCoordinates