OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorWholeFutureSigma.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

One predecessor restores exactly one level of the whole future

  1. abbrev OAI.DukePrimeDegree.fullFutureSigma line 12
  2. lemma OAI.DukePrimeDegree.fullFutureSigma_one line 16
  3. lemma OAI.DukePrimeDegree.fullFutureSigma_comap line 21
  4. lemma OAI.DukePrimeDegree.fullFutureSigma_zero line 34
  5. lemma OAI.DukePrimeDegree.futureLabelBlock_shift_generate line 40
  6. lemma OAI.DukePrimeDegree.futureLabelBlock_shift_monotone line 47
  7. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_chain_fullFuture line 53
  8. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_comp_preserving_fullFuture line 68
  9. theorem OAI.DukePrimeDegree.fullFutureSigma_predecessor line 81
  10. theorem OAI.DukePrimeDegree.fullFutureSigma_predecessor_at line 106