OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTiledProbeBoxes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PolycyclicRecognition.CartanWordModel.TiledProbeBoxData line 29

   Source documentation

   Fixed source box data; packaging it keeps later three-chain applications small when the ambient algebra is an actual tangent Lie algebra.

   structure TiledProbeBoxData
       (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
       (ExpN : GroupLieAlgebra (𝓘(ℝ, EN)) N → N)
       (ExpI : M.coneWordIdeal C → I) (ι : I →* N)
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Fin 3 → Set W) (β : Fin 3 → M.ConeIdealBases C) where
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_tiled_probe_boxes line 73

   Source documentation

   The ideal-section sampler and both reverse-flow samplers lie in the three actual ambient word boxes. Their bases and the first radius are chosen uniformly before the scale, partition and flow.

   theorem exists_tiled_probe_boxes
       (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
       (ExpN : GroupLieAlgebra (𝓘(ℝ, EN)) N → N) (hExpN : IsGroupExponential ExpN)
       (chartN : GroupLieAlgebra (𝓘(ℝ, EN)) N ≃ₜ N) (hchartN : ∀ v, chartN v = ExpN v)
       (dynkinN : NilpotentDynkinExpansionInput EN N)
       (ExpI : M.coneWordIdeal C → I) (ι : I →* N) (hι : Measurable ι)
       (hcompat : ∀ v, ι (ExpI v) = ExpN (eN (v : cartanRootIdeal H)))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (E : Fin 3 → Set W)
       (hs : ∀ j i, 0 ≤ (M.supportIn T hunimod eW).weightSupport (E j) i)
       (hzero : ∀ j i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
   …

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

3. theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_tiledProbeBoxData line 190