OAI/Computability/VertexCover/Information/Finite.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Information.IsProbability line 11
  2. def OAI.UniqueGames.Foundations.Information.SupportedBy line 14
  3. def OAI.UniqueGames.Foundations.Information.relativeEntropy line 16
  4. def OAI.UniqueGames.Foundations.Information.totalVariation line 19
  5. def OAI.UniqueGames.Foundations.Information.posterior line 22
  6. theorem OAI.UniqueGames.Foundations.Information.posterior_isProbability line 25
  7. theorem OAI.UniqueGames.Foundations.Information.posterior_supportedBy line 35
  8. theorem OAI.UniqueGames.Foundations.Information.mul_log_div_ge_sub line 40
  9. theorem OAI.UniqueGames.Foundations.Information.relativeEntropy_nonneg line 48
  10. theorem OAI.UniqueGames.Foundations.Information.posterior_relativeEntropy_le line 60
  11. theorem OAI.UniqueGames.Foundations.Information.totalVariation_nonneg line 84
  12. theorem OAI.UniqueGames.Foundations.Information.totalVariation_symm line 87
  13. theorem OAI.UniqueGames.Foundations.Information.totalVariation_le_one line 90
  14. theorem OAI.UniqueGames.Foundations.Information.le_binaryLog_of_le_log line 101
  15. theorem OAI.UniqueGames.Foundations.Information.weighted_sum_sq_le line 111