OAI/NumberTheory/DukePrimeDegree/Entropy/AuxiliaryKernelEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary-future upper bound in terms of the actual kernel

  1. lemma OAI.DukePrimeDegree.combined_future_kernel_entropy_le line 13
  2. theorem OAI.DukePrimeDegree.predecessor_auxiliary_kernel_entropyRate_le line 43