OAI/NumberTheory/PrimePackets/GeneratingObservationEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entropy approximation by generating finite observations

The increasing sigma algebras of a generating sequence exhaust each measurable finite observation. Martingale convergence, followed by bounded convergence of finite Shannon entropy, makes the conditional entropy vanish.

  1. theorem OAI.PrimeDegreePackets.observationConditionalProbability_tendsto line 22
  2. theorem OAI.PrimeDegreePackets.conditionalObservationEntropy_tendsto_zero line 48