OAI/Probability/SKRatio/Entropy/ProductEntropy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Observation.productPrior line 15
  2. lemma OAI.SKRatio.Observation.productPrior_pos line 22
  3. lemma OAI.SKRatio.Observation.sum_cons line 27
  4. lemma OAI.SKRatio.Observation.avg_product_succ line 32
  5. lemma OAI.SKRatio.Observation.avg_swap line 39
  6. lemma OAI.SKRatio.Observation.entropy_product_chain line 50
  7. lemma OAI.SKRatio.Observation.update_cons_succ line 69
  8. def OAI.SKRatio.Observation.productSiteEntropy line 79
  9. lemma OAI.SKRatio.Observation.productSiteEntropy_zero line 82
  10. lemma OAI.SKRatio.Observation.productSiteEntropy_succ line 90
  11. theorem OAI.SKRatio.Observation.product_entropy_tensorization line 97
  12. lemma OAI.SKRatio.Observation.invariant_update line 127
  13. lemma OAI.SKRatio.Observation.avg_product_resample line 136
  14. theorem OAI.SKRatio.Observation.product_entropy_le_remainders line 155
  15. def OAI.SKRatio.Fields.sitePrior line 182
  16. lemma OAI.SKRatio.Fields.sitePrior_avg line 190
  17. lemma OAI.SKRatio.Fields.conditionalExpectation_pos line 198
  18. lemma OAI.SKRatio.Fields.conditionalExpectation_log_le line 204
  19. lemma OAI.SKRatio.Fields.single_remainder_le_energy line 211
  20. theorem OAI.SKRatio.Fields.remainders_le_energy line 226