OAI/NumberTheory/DukePrimeDegree/Geometry/RootFiberReference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A common sampled reference on each independent root fiber

  1. def OAI.DukePrimeDegree.InitialRootStep.rootFiberPoint line 16
  2. lemma OAI.DukePrimeDegree.InitialRootStep.measurable_rootFiberPoint line 20
  3. lemma OAI.DukePrimeDegree.InitialRootStep.rootFiberPoint_translate line 26
  4. theorem OAI.DukePrimeDegree.InitialRootStep.exists_common_nextProduct_reference line 36