OAI/NumberTheory/DukePrimeDegree/Entropy/KernelFutureInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual root information is bounded by full metric entropy

The entire future is an almost sure fiber label of the constructed kernel. Adding that label to the conditioning sigma algebra leaves its conditional law unchanged, and makes the future inclusion literal.

  1. theorem OAI.DukePrimeDegree.EliminationChain.ambientFutureMeasure_ae_same_names line 23
  2. theorem OAI.DukePrimeDegree.EliminationChain.wholeFuture_rootSum_le_metricEntropy line 45