OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPolarConeAction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.factor_action_eq_adjoint line 30
2. theorem OAI.PolycyclicRecognition.CartanWordModel.sum_height_weights_transport line 51
3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_cone_ambient_action line 61

   Source documentation

   Salience removes the cone vertex at the generators, giving the actual ambient action without a false zero-exclusion assumption on a closed cone.

   theorem exists_polar_cone_ambient_action
       (j : GroupLieAlgebra (𝓘(ℝ, EG)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
       (hρ : Function.Injective ρ)
       (hN : ∀ x : cartanRootIdeal H,
         ρ (F.inclusionN (F.ExpN (F.N.equiv x))) = algebraExpUnit (j x))
       (hD : ∀ h : H, ρ (F.inclusionD (F.ExpD (F.D.equiv h))) = algebraExpUnit (j h))
       (hNbij : Function.Bijective F.ExpN) (hDsurj : Function.Surjective F.ExpD)
       (dynkin : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (K : ProperCone ℝ (StrongDual ℝ W))
       (hK : (K : ConvexCone ℝ (StrongDual ℝ W)).Salient)
       (π : F.N.carrier →* Q) (s : Q → F.N.carrier) (hs : Function.RightInverse s π)
       (hker : (π.ker : Set F.N.carrier) = F.ExpN ''
   …

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

4. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_cone_action_haar line 91

   Source documentation

   The descended action comes with its genuine Haar measure and the exact positive generator multiplicities used by the offset trace separation.

   theorem exists_polar_cone_action_haar
       (j : GroupLieAlgebra (𝓘(ℝ, EG)) G →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ)
       (hρ : Function.Injective ρ)
       (hN : ∀ x : cartanRootIdeal H,
         ρ (F.inclusionN (F.ExpN (F.N.equiv x))) = algebraExpUnit (j x))
       (hD : ∀ h : H, ρ (F.inclusionD (F.ExpD (F.D.equiv h))) = algebraExpUnit (j h))
       (hNbij : Function.Bijective F.ExpN) (hDbij : Function.Bijective F.ExpD)
       (dynkin : NilpotentDynkinExpansionInput F.N.modelSpace F.N.carrier)
       (K : ProperCone ℝ (StrongDual ℝ W))
       (hK : (K : ConvexCone ℝ (StrongDual ℝ W)).Salient)
       (Q₀ : NilpotentLieModel ((cartanRootIdeal H) ⧸
         M.coneWordIdeal (heightConePreimage T eW K)))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage