OAI/NumberTheory/DukePrimeDegree/Entropy/RootPrefixFutureFibers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive future fibers for the remaining-root product charts

  1. def OAI.DukePrimeDegree.EliminationChain.fullRootTime line 18
  2. lemma OAI.DukePrimeDegree.EliminationChain.continuous_fullRootTime line 25
  3. lemma OAI.DukePrimeDegree.EliminationChain.fullRootTime_zero line 30
  4. lemma OAI.DukePrimeDegree.EliminationChain.word_fullRootTime line 38
  5. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.futureFiber_mem_nhds line 49
  6. theorem OAI.DukePrimeDegree.RootPrefixBox.ae_mem_conditionalKernel_support line 82
  7. theorem OAI.DukePrimeDegree.exists_cuts_with_positive_rootPrefix_future_fibers line 94