OAI/NumberTheory/DukePrimeDegree/Entropy/WholeFutureConditionalInformation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual conditional information of the whole-future root kernel

  1. theorem OAI.DukePrimeDegree.selfConstant_kernel_conditionalInformation line 17
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom_present_inter_one line 32
  3. theorem OAI.DukePrimeDegree.EliminationChain.wholeFuture_conditionalInformation line 48
  4. theorem OAI.DukePrimeDegree.EliminationChain.wholeFuture_conditionalInformation_integrable_integral line 85