OAI/NumberTheory/DukePrimeDegree/Geometry/QuotientSeparatingCuts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Countable separating distance cuts on the lattice quotient

Distance cuts can be chosen in every rational interval. Together with a countable dense set of centers they separate points. Their finite prefixes therefore generate the Borel sigma algebra, while the good-cut construction keeps every finite future itinerary locally constant along upper roots.

  1. abbrev OAI.DukePrimeDegree.RationalCutInterval line 20
  2. abbrev OAI.DukePrimeDegree.QuotientCutIndex line 21
  3. instance OAI.DukePrimeDegree.(instance at line 23) line 23
  4. def OAI.DukePrimeDegree.quotientCutBit line 25
  5. lemma OAI.DukePrimeDegree.quotientCutBit_measurable line 29
  6. theorem OAI.DukePrimeDegree.quotientCutBit_injective line 39
  7. theorem OAI.DukePrimeDegree.quotientCutBit_measurableEmbedding line 74
  8. theorem OAI.DukePrimeDegree.exists_good_quotient_cuts line 80