OAI/Probability/ThreeState/Entropy.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Message entropy and its integrability.

  1. lemma OAI.ThreeState.average_message line 14
  2. lemma OAI.ThreeState.message_last line 17
  3. lemma OAI.ThreeState.avg_nonneg line 22
  4. lemma OAI.ThreeState.avg_le_const line 25
  5. lemma OAI.ThreeState.abs_avg_le line 29
  6. lemma OAI.ThreeState.edgeMessage_bounds line 39
  7. lemma OAI.ThreeState.edgeMessage_pos line 44
  8. lemma OAI.ThreeState.productWeight_bounds line 49
  9. lemma OAI.ThreeState.normalizer_bounds line 63
  10. lemma OAI.ThreeState.normalizer_pos line 73
  11. lemma OAI.ThreeState.combineMessage_pos line 77
  12. lemma OAI.ThreeState.continuous_combineMessage_positive line 83
  13. lemma OAI.ThreeState.positive_fixedpoint line 88
  14. def OAI.ThreeState.edgeLogBound line 99
  15. lemma OAI.ThreeState.edgeLogBound_nonneg line 101
  16. lemma OAI.ThreeState.abs_log_of_bounds line 103
  17. lemma OAI.ThreeState.log_combineMessage line 120
  18. lemma OAI.ThreeState.log_combineMessage_bound line 130
  19. def OAI.ThreeState.mLog line 145
  20. def OAI.ThreeState.mCenteredLog line 146
  21. def OAI.ThreeState.entropyI line 147
  22. def OAI.ThreeState.entropyJ line 148
  23. def OAI.ThreeState.entropyB line 149
  24. def OAI.ThreeState.entropyF line 150
  25. lemma OAI.ThreeState.measurable_mLog line 152
  26. lemma OAI.ThreeState.measurable_avg line 154
  27. lemma OAI.ThreeState.measurable_mCenteredLog line 158
  28. lemma OAI.ThreeState.measurable_entropyI line 160
  29. lemma OAI.ThreeState.measurable_entropyJ line 162
  30. lemma OAI.ThreeState.measurable_entropyB line 164
  31. lemma OAI.ThreeState.measurable_entropyF line 166
  32. lemma OAI.ThreeState.centeredLog_combine line 170
  33. lemma OAI.ThreeState.centeredLog_J line 177
  34. lemma OAI.ThreeState.entropyF_radial line 181
  35. lemma OAI.ThreeState.centeredLog_bound line 186
  36. lemma OAI.ThreeState.entropyI_bound line 193
  37. lemma OAI.ThreeState.entropyJ_bound line 199
  38. lemma OAI.ThreeState.entropyB_nonneg line 210
  39. lemma OAI.ThreeState.entropyB_bound line 213
  40. lemma OAI.ThreeState.continuous_avg line 233
  41. lemma OAI.ThreeState.continuous_mLog_edge line 238
  42. lemma OAI.ThreeState.continuous_mCenteredLog_edge line 243
  43. lemma OAI.ThreeState.continuous_entropyI_edge line 248
  44. lemma OAI.ThreeState.continuous_entropyJ_edge line 254
  45. lemma OAI.ThreeState.continuous_entropyB_edge line 260
  46. lemma OAI.ThreeState.integrable_mLog_fixedpoint line 266
  47. lemma OAI.ThreeState.integrable_entropyI_fixedpoint line 278
  48. lemma OAI.ThreeState.integrable_entropyJ_fixedpoint line 290
  49. lemma OAI.ThreeState.integrable_entropyB_fixedpoint line 302
  50. lemma OAI.ThreeState.integrable_entropyF_fixedpoint line 314