OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorWordEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite predecessor words control clipped countable words

  1. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_le_of_fiber_refinement line 12
  2. theorem OAI.DukePrimeDegree.predecessor_clippedWord_conditionalEntropy_le line 33