OAI/NumberTheory/DukePrimeDegree/Geometry/RootVectorDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed vectors on finite-volume root orbits

A finite distribution invariant under a root shear is supported on the fixed hyperplane of that shear. Recurrence proves this directly. Applied to the vector orbit map, it shows that a vector fixed by the actual lattice stabilizer is fixed by every root group in the orbit group. This is the fixed-vector part of the density argument used to exclude singleton root blocks.

  1. def OAI.DukePrimeDegree.rootVectorAction line 24
  2. lemma OAI.DukePrimeDegree.continuous_rootVectorAction line 27
  3. lemma OAI.DukePrimeDegree.rootVectorAction_iterate line 34
  4. theorem OAI.DukePrimeDegree.ae_rootVector_fixed_of_map_eq line 47
  5. def OAI.DukePrimeDegree.fixedVectorOrbitMap line 72
  6. lemma OAI.DukePrimeDegree.continuous_fixedVectorOrbitMap line 85
  7. lemma OAI.DukePrimeDegree.fixedVectorOrbitMap_rightAction line 92
  8. theorem OAI.DukePrimeDegree.fixedVector_root_coordinate_zero_of_finite_orbit line 101