OAI/NumberTheory/DukePrimeDegree/Entropy/FutureBlockConditionalInformation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Information of finite words against delayed future kernels

  1. lemma OAI.DukePrimeDegree.EliminationChain.remainingFutureAtom_word_inter line 16
  2. theorem OAI.DukePrimeDegree.EliminationChain.futureBlock_conditionalProbability line 39
  3. theorem OAI.DukePrimeDegree.EliminationChain.futureBlock_conditionalInformation line 77
  4. theorem OAI.DukePrimeDegree.delayedFuture_conditionalInformation_integrable_integral line 100