OAI/NumberTheory/DukePrimeDegree/Entropy/PredecessorFutureInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Countable future information controls full entropy

Finite predecessor symbols identify the integrable information of the countable present given its entire future. Neutral bilateral fibers then allow the bound to pass to every finite observation on the quotient.

  1. theorem OAI.DukePrimeDegree.finite_predecessors_future_information_upper line 20
  2. theorem OAI.DukePrimeDegree.diagonal_entropy_le_countable_future_information line 50