OAI/NumberTheory/DukePrimeDegree/Entropy/CountableConditioningChain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Chain rules with one countable conditioning label

Finite clipping of the conditioning label and the martingale limit extend the finite chain rule without requiring finite entropy of that label.

  1. lemma OAI.DukePrimeDegree.observationSigma_pair_eq line 17
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_chain_nat line 30
  3. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_comp_preserving_nat line 63