OAI/NumberTheory/PrimePackets/ObservationConditionalProbability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conditional probabilities of finite observations

The conditional entropy is the integral of the entropy of the actual finite conditional distributions. Zero-mass conditioning cells contribute zero, without requiring arbitrary probability distributions on them.

  1. def OAI.PrimeDegreePackets.observationConditionalProbability line 21
  2. lemma OAI.PrimeDegreePackets.observationConditionalProbability_nonneg line 26
  3. lemma OAI.PrimeDegreePackets.observationConditionalProbability_le_one line 32
  4. lemma OAI.PrimeDegreePackets.observationConditionalProbability_sum line 42
  5. lemma OAI.PrimeDegreePackets.observationConditionalProbability_ae_sum line 53
  6. theorem OAI.PrimeDegreePackets.conditionalObservationEntropy_eq_sum line 61
  7. theorem OAI.PrimeDegreePackets.conditionalObservationEntropy_eq_integral line 75