OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalFiberRecoding.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite recoding within the fibers of a countable observation

  1. lemma OAI.DukePrimeDegree.observationEntropy_eq_of_ae_eq line 14
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_le_fiber_recoding line 25
  3. theorem OAI.DukePrimeDegree.predecessor_clip_conditionalEntropy_le line 56