OAI/NumberTheory/DukePrimeDegree/Geometry/RootHorosphereGroup.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two-step horospherical group used in the low-entropy argument

The shearing shape is a closed subgroup of the special linear group. Its displacement matrices have products supported only at the selected root entry. These elementary facts provide the group on which the remaining conditional-support argument is carried out.

  1. lemma OAI.DukePrimeDegree.sparse_root_product_entry_zero line 21
  2. lemma OAI.DukePrimeDegree.rootHorosphere_displacement_shape line 48
  3. theorem OAI.DukePrimeDegree.rootHorosphere_product_displacement_zero line 54
  4. theorem OAI.DukePrimeDegree.rootHorosphereShape_mul line 62
  5. theorem OAI.DukePrimeDegree.rootHorosphere_inverse_matrix line 85
  6. theorem OAI.DukePrimeDegree.rootHorosphereShape_inv line 101
  7. def OAI.DukePrimeDegree.rootHorosphereGroup line 117
  8. theorem OAI.DukePrimeDegree.isClosed_rootHorosphereGroup line 123