OAI/NumberTheory/DukePrimeDegree/Entropy/CountableConditionalInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Information of the countable present given its future

A binary recoding gives each individual conditional probability. Since there are only countably many present labels, all of them hold together outside one null set.

  1. theorem OAI.DukePrimeDegree.conditionalProbability_countablePresentFutureFiber line 22
  2. theorem OAI.DukePrimeDegree.conditionalInformation_countablePresentFutureFiber line 38