OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixLeafMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Locally finite leaf measures on each remaining subgroup

The actual prefix-box kernels glue through their normalized restrictions on a countable long-box exhaustion. No root-product identity is assumed.

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_exists_prefixLeafMeasure line 23
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.prefixLeafMeasure_unique line 109