OAI/NumberTheory/DukePrimeDegree/Entropy/CountableFutureInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Information of finite labels given the countable future

Conditional probabilities are actual leaf mass ratios, and their logarithms are integrable for each finite present observation.

  1. theorem OAI.DukePrimeDegree.conditionalProbability_countableFutureFiber line 21
  2. theorem OAI.DukePrimeDegree.countableFutureFiber_information_integrable_integral line 43