OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalSigmaLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entropy along increasing conditioning sigma algebras

The martingale limit applies also when the conditioning includes an arbitrary transverse coordinate in addition to finite future names.

  1. lemma OAI.DukePrimeDegree.finiteShannon_norm_le_card_of_unit_bounds line 17
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_tendsto_iSup line 31