OAI/NumberTheory/DukePrimeDegree/Entropy/CountableFutureCodes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite codes converging to the future of a countable observation

Both the time interval and the clipping level increase. The limiting atom records every future value of the original countable observation.

  1. def OAI.DukePrimeDegree.countableFutureCode line 17
  2. lemma OAI.DukePrimeDegree.countableFutureCode_measurable line 21
  3. def OAI.DukePrimeDegree.truncateCountableFutureCode line 27
  4. lemma OAI.DukePrimeDegree.truncate_countableFutureCode line 35
  5. lemma OAI.DukePrimeDegree.countableFutureCode_eq_of_longer line 46
  6. lemma OAI.DukePrimeDegree.all_countableFutureCode_eq_iff line 53
  7. lemma OAI.DukePrimeDegree.transverse_countableFutureCode_monotone line 75
  8. lemma OAI.DukePrimeDegree.countableFutureCode_fibers_antitone line 90
  9. def OAI.DukePrimeDegree.countableFutureFiber line 96
  10. lemma OAI.DukePrimeDegree.countableFutureFiber_eq_iInter line 100