CartanPolarFlowTiling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Strict-width tiling for the actual polar probe templates

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_flow_tiling line 36

Source documentation

The source tiling has the exact three polar radii. Its reverse anchors use the inverse of the actual conjugating automorphism, and its number of tiles has exponent (b-a) times the fixed polar ideal exponent.

theorem exists_polar_flow_tiling
    (eI : M.coneWordIdeal C ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EI)) I)
    (ExpI : GroupLieAlgebra (𝓘(ℝ, EI)) I → I) (hExpI : IsGroupExponential ExpI)
    (chartI : GroupLieAlgebra (𝓘(ℝ, EI)) I ≃ₜ I) (hchartI : ∀ v, chartI v = ExpI v)
    (dynkinI : NilpotentDynkinExpansionInput EI I)
    (haarI : NilpotentExponentialHaarInput EI I)
    (ι : I →* N) (hι : Function.Injective ι)
    (ExpN : cartanRootIdeal H → N)
    (hcompat : ∀ v : M.coneWordIdeal C, ι (ExpI (eI v)) = ExpN v)
    (j : cartanRootIdeal H →ₗ⁅ℝ⁆ A) (ρ : N →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (ExpN x) = algebraExpUnit (j x))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit