OAI/NumberTheory/DukePrimeDegree/Entropy/FutureSigmaAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact transverse and future conditioning sigma algebra

  1. lemma OAI.DukePrimeDegree.transverseLabelSigma_eq_sup line 12
  2. lemma OAI.DukePrimeDegree.finiteFutureCode_sigma line 18
  3. lemma OAI.DukePrimeDegree.observationSigma_comp_eq_comap line 23
  4. theorem OAI.DukePrimeDegree.transverseFutureSigma_eq_sup line 27
  5. theorem OAI.DukePrimeDegree.transverse_future_entropy_le line 38