OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixRegionCandidates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Based remaining-group measures determine kernels on region overlaps

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.conditional_overlap_of_based_measure line 19
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.conditional_of_region_time_cover line 49
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.conditional_of_region_contained line 85