CartanPolarSourceFrames.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual linked frames on the counted polar source cell

abbrev OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.LinkedSource line 80
Source documentation
The linked frames on this exact source cell.
```
abbrev PolarTiledSamplerData.LinkedSource :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.source_section_rightInverse line 91
Source documentation
The section kept by the counted source sampler is a right inverse of its actual quotient homomorphism.
```
theorem PolarTiledSamplerData.source_section_rightInverse
    (hchartN : ∀ v, chartN v = F.ExpN v) :
    ∀ q, D.maps.quotient (σ q) = q := by
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.nonempty_linkedSource line 110

Source documentation

The prescribed polar sampler and original neighboring boxes construct all linked source frames, including their exact counted tile endpoints.

theorem PolarTiledSamplerData.nonempty_linkedSource
    (hε : 0 ≤ ε)
    (hbijN : Function.Bijective F.ExpN)
    (hchartN : ∀ v, chartN v = F.ExpN v)
    (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
    (dynkinN : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
    {Eall : Set W} (hEall : IsCompact Eall) (hne : Eall.Nonempty)
    (γ : M.Bases)
    (hγ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList bN)
      (M.boxCost T hunimod eW Eall) γ.val)
    (w : W) (hBE : (fun z => z + w) '' normalizedPolarTemplates K ε 1 ⊆ Eall)
    (hw : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport Eall i)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.normalizedPolarTemplates