OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalMapEntropy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy conditioned on a measurable observation

  1. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_comap_eq_integral line 14
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_comap_nonneg line 45
  3. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_comap_le_reference_bad_sets line 55