OAI/NumberTheory/DukePrimeDegree/Geometry/RowCubes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Rectangular row boxes

Sup-norm row cubes split into a remaining-coordinate cube and a real interval. Free row orbits admit boxes with exactly these time domains, so the row-to-single-root coordinate change preserves product boxes.

  1. def OAI.DukePrimeDegree.rowCube line 21
  2. def OAI.DukePrimeDegree.rowRemainingCube line 24
  3. lemma OAI.DukePrimeDegree.rowCube_eq_ball line 27
  4. lemma OAI.DukePrimeDegree.isOpen_rowCube line 36
  5. lemma OAI.DukePrimeDegree.isOpen_rowRemainingCube line 39
  6. theorem OAI.DukePrimeDegree.rowTimeSplit_cube line 48
  7. theorem OAI.DukePrimeDegree.rowRootBox_with_cube_time line 76