OAI/NumberTheory/DukePrimeDegree/Geometry/FirstCoverCode.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

One covering label instead of the full vector of cut tests

A point is labeled by one cut containing it. There are N+1 labels for N cuts. Equality of labels still puts covered points in the same small set, while constancy of all cut tests implies constancy of this label.

  1. def OAI.DukePrimeDegree.firstTrue line 16
  2. lemma OAI.DukePrimeDegree.firstTrue_common line 19
  3. def OAI.DukePrimeDegree.firstCoverCode line 35
  4. lemma OAI.DukePrimeDegree.firstCoverCode_measurable line 39
  5. lemma OAI.DukePrimeDegree.firstCoverCode_eq_of_cutCode_eq line 49
  6. lemma OAI.DukePrimeDegree.firstCoverCode_selected line 56
  7. lemma OAI.DukePrimeDegree.firstCoverCode_common line 66
  8. lemma OAI.DukePrimeDegree.layered_firstCover_eq_of_cutCode_eq line 77