OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryRetainedRay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_retained_generator_for_template_ray line 32

   Source documentation

   A pulled-back target weight retains a genuine source generator. This supplies both the nonzero ray needed for the descended action and the strict positivity of its Haar character.

   theorem exists_retained_generator_for_template_ray
       (A : templateSymmetryGroup (M.supportIn T hunimod eW)) (i : Fin M.letterCount) :
       let χ := ((α i).comp A.val.toLinearMap).comp θ
   …

   Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup

2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_negative_sampling_weight line 56

   Source documentation

   The selected nonzero target weight has a contracting direction in height space.

   theorem exists_negative_sampling_weight (i : Fin M.letterCount) :
       ∃ w : W, α i w < 0 := by
   …