CartanPolarTiledChains.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The three actual chains for the polar flow partition

def OAI.PolycyclicRecognition.normalizedPolarTemplates line 12

Source documentation

Normalized templates ordered as source, reverse anchor, within-tile.

def normalizedPolarTemplates {W : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (K : ProperCone ℝ (StrongDual ℝ W)) (ε : ℝ) (j : Fin 3) : Set W :=
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_tiled_probe_chains line 44
Source documentation
The same maximal polar ideal basis from the flow tiling supplies all three actual measurable chain families. Their common ambient basis and amplitude envelope are constructed from the largest polar radius.
```
theorem exists_polar_tiled_probe_chains
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput