OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootBasedMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Full upper-root measures normalized at their current point

  1. lemma OAI.DukePrimeDegree.EliminationChain.zeroTime_mem_cube line 15
  2. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_unit_pos line 24
  3. def OAI.DukePrimeDegree.basedUpperRootMeasure line 35
  4. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_unit line 39
  5. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_locallyFinite line 50
  6. def OAI.DukePrimeDegree.centerUpperRootKernel line 62
  7. def OAI.DukePrimeDegree.basedUpperRootKernel line 76
  8. def OAI.DukePrimeDegree.UpperRootBox.basedLeaf line 92
  9. lemma OAI.DukePrimeDegree.UpperRootBox.aemeasurable_basedLeaf line 96
  10. theorem OAI.DukePrimeDegree.UpperRootBox.ae_basedLeaf_spec line 108