OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootNormalizedLeaves.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Chosen normalized full upper-root leaf measures

The projectively compatible box conditionals determine locally finite measures on all upper-root times. Their normalization is independent of the exhaustion radius and their restrictions agree with every larger box.

  1. def OAI.DukePrimeDegree.UpperRootBox.IsNormalizedUpperRootLeaf line 23
  2. def OAI.DukePrimeDegree.UpperRootBox.leafMeasure line 33
  3. lemma OAI.DukePrimeDegree.UpperRootBox.leafMeasure_spec_of_exists line 37
  4. theorem OAI.DukePrimeDegree.UpperRootBox.ae_leafMeasure_spec line 44
  5. lemma OAI.DukePrimeDegree.UpperRootBox.IsNormalizedUpperRootLeaf.unique line 54
  6. lemma OAI.DukePrimeDegree.UpperRootBox.IsNormalizedUpperRootLeaf.ne_zero line 61
  7. theorem OAI.DukePrimeDegree.UpperRootBox.ae_leafMeasure_restrict line 69
  8. theorem OAI.DukePrimeDegree.UpperRootBox.ae_leafMeasure_radius_independent line 121