OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootLeafMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Locally finite conditional measures on complete upper-root leaves

The finite-box conditionals have compatible normalized restrictions. Their increasing limit is a locally finite measure on all real root coordinates, uniquely determined by the countable long-box atlas.

  1. lemma OAI.DukePrimeDegree.subgroup_free_of_free_translate line 20
  2. theorem OAI.DukePrimeDegree.UpperRootBox.ae_injective_upperRoot_slice_of_ae_free line 37
  3. theorem OAI.DukePrimeDegree.UpperRootBox.ae_exists_upperRootLeafMeasure line 56
  4. theorem OAI.DukePrimeDegree.UpperRootBox.upperRootLeafMeasure_unique line 142