OAI/NumberTheory/DukePrimeDegree/Geometry/PhysicalPrefixMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Independent physical rectangles in the full prefix coordinates

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixMeasure line 18
  2. instance OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixMeasure_finite line 26
  3. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixMeasure_independent line 36
  4. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixMeasure_ae_rectangle line 64
  5. def OAI.DukePrimeDegree.RootPrefixCoordinates.unrestrictedPrefixBasePoint line 73
  6. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.continuous_unrestrictedPrefixBasePoint line 77
  7. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.map_physicalPrefixMeasure line 82
  8. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixMeasure_map_exchange line 105