OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixNormalizedLeaves.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Normalized remaining-subgroup leaf measures

The chosen measure is characterized by actual prefix-box conditionals, and is independent of the exhaustion radius.

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