OAI/NumberTheory/DukePrimeDegree/Entropy/ObservationInformation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Integrable pointwise information of finite observations

  1. def OAI.DukePrimeDegree.observationInformation line 13
  2. theorem OAI.DukePrimeDegree.observationInformation_integrable line 17
  3. theorem OAI.DukePrimeDegree.integral_observationInformation line 22
  4. lemma OAI.DukePrimeDegree.observationInformation_nonneg line 35
  5. lemma OAI.DukePrimeDegree.measurable_kernel_observationInformation line 40
  6. theorem OAI.DukePrimeDegree.integrable_kernel_observationInformation line 61
  7. theorem OAI.DukePrimeDegree.conditionalEntropy_fst_information line 84