OAI/NumberTheory/DukePrimeDegree/Entropy/CountableFutureFiberEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual leaf entropy conditioned on a countable future

Finite time-and-label approximations identify the conditional entropy of any finite present label with the entropy of the actual leaf kernel restricted to its positive-mass countable future atom.

  1. theorem OAI.DukePrimeDegree.conditionalEntropy_countableFutureFiber line 19
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalEntropy_countableFuture_intrinsicProduct line 51