OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalInformation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Conditional entropy as the mean pointwise information

The finite observed variable has a regular conditional distribution even when the conditioning sigma algebra is arbitrary. Lifting its underlying space keeps the ambient and conditioning measurable structures distinct.

  1. def OAI.DukePrimeDegree.conditionalInformation line 17
  2. theorem OAI.DukePrimeDegree.conditionalInformation_integrable_integral line 21