OAI/NumberTheory/PrimePackets/FutureEntropyIncrements.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conditional entropy increments of stationary finite observations

  1. def OAI.PrimeDegreePackets.futureName line 15
  2. lemma OAI.PrimeDegreePackets.futureName_measurable_fiber line 19
  3. lemma OAI.PrimeDegreePackets.orbitEntropy_succ_head line 24
  4. lemma OAI.PrimeDegreePackets.futureConditionalEntropy_eq_sub line 37
  5. lemma OAI.PrimeDegreePackets.futureConditionalEntropy_antitone line 49
  6. lemma OAI.PrimeDegreePackets.sum_futureConditionalEntropy line 58
  7. theorem OAI.PrimeDegreePackets.futureConditionalEntropy_tendsto_rate line 70