OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalSigmaOrder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conditioning on more measurable information decreases entropy

Conditional Jensen and the tower property apply directly to the actual conditional expectations defining finite-observation entropy.

  1. lemma OAI.DukePrimeDegree.integrable_negMulLog_of_unit_bounds line 18
  2. lemma OAI.DukePrimeDegree.conditionalProbability_unit_bounds line 29
  3. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_antitone line 44