OAI/NumberTheory/DukePrimeDegree/Entropy/FiniteFutureCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite codes for actual future observations

  1. def OAI.DukePrimeDegree.finiteFutureCode line 13
  2. lemma OAI.DukePrimeDegree.finiteFutureCode_measurable line 17
  3. def OAI.DukePrimeDegree.truncateFutureCode line 25
  4. lemma OAI.DukePrimeDegree.truncate_finiteFutureCode line 30
  5. lemma OAI.DukePrimeDegree.finiteFutureCode_eq_of_longer line 36
  6. lemma OAI.DukePrimeDegree.all_finiteFutureCode_eq_iff line 42
  7. lemma OAI.DukePrimeDegree.transverse_finiteFutureCode_monotone line 56
  8. lemma OAI.DukePrimeDegree.finiteFutureCode_fibers_antitone line 71