OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorWholeFutureEntropy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact predecessor-word entropy conditioned on the whole terminal future

  1. def OAI.DukePrimeDegree.fullFutureObservation line 12
  2. lemma OAI.DukePrimeDegree.fullFutureObservation_measurable line 15
  3. lemma OAI.DukePrimeDegree.fullFutureSigma_eq_comap line 20
  4. lemma OAI.DukePrimeDegree.orbitName_eq_iff_last_initial line 25
  5. theorem OAI.DukePrimeDegree.predecessor_word_wholeFuture_increment line 40
  6. theorem OAI.DukePrimeDegree.predecessor_word_wholeFuture_entropy line 81