OAI/NumberTheory/DukePrimeDegree/Entropy/RemainingFutureShift.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact shift of future atoms along remaining-root leaves

  1. def OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom line 16
  2. lemma OAI.DukePrimeDegree.EliminationChain.measurableSet_remainingFutureAtom line 23
  3. lemma OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom_zero_subset_one line 39
  4. lemma OAI.DukePrimeDegree.EliminationChain.remaining_orbit_diagonal line 45
  5. theorem OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom_shift line 55