OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixBasedMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measurable remaining-subgroup leaves based at the sampled point

  1. def OAI.DukePrimeDegree.EliminationChain.centeredRemainingKernel line 15
  2. def OAI.DukePrimeDegree.EliminationChain.basedRemainingKernel line 30
  3. lemma OAI.DukePrimeDegree.EliminationChain.groupLeafMeasure_centered line 45
  4. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.timeParam_rebased line 66
  5. def OAI.DukePrimeDegree.RootPrefixBox.basedLeaf line 86
  6. lemma OAI.DukePrimeDegree.RootPrefixBox.aemeasurable_basedLeaf line 91
  7. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_basedLeaf_spec line 102