OAI/Probability/ThreeState/PosteriorMoments.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Posterior deviation moments and positive-channel estimates.

  1. def OAI.ThreeState.messageDeviation line 14
  2. def OAI.ThreeState.messageX line 15
  3. def OAI.ThreeState.messageY line 16
  4. lemma OAI.ThreeState.avg_messageDeviation line 18
  5. lemma OAI.ThreeState.messageX_nonneg line 23
  6. lemma OAI.ThreeState.messageX_le_one line 25
  7. lemma OAI.ThreeState.continuous_messageX line 31
  8. lemma OAI.ThreeState.continuous_messageY line 35
  9. lemma OAI.ThreeState.integrable_continuous_message line 39
  10. lemma OAI.ThreeState.entropyJ_functionJ line 42
  11. lemma OAI.ThreeState.messageDeviation_edge line 45
  12. lemma OAI.ThreeState.entropyJ_nonneg line 50
  13. def OAI.ThreeState.messageA line 60
  14. def OAI.ThreeState.messageQ line 61
  15. lemma OAI.ThreeState.messageA_eq_resolvent line 64
  16. lemma OAI.ThreeState.messageQ_eq_resolvent line 69
  17. lemma OAI.ThreeState.messageA_lower line 77
  18. lemma OAI.ThreeState.messageQ_lower line 82
  19. lemma OAI.ThreeState.messageY_upper line 87
  20. lemma OAI.ThreeState.integral_continuous_cauchy line 96
  21. def OAI.ThreeState.posteriorMu line 117
  22. def OAI.ThreeState.posteriorNu line 118
  23. def OAI.ThreeState.posteriorEta line 119
  24. lemma OAI.ThreeState.posteriorMu_nonneg line 121
  25. lemma OAI.ThreeState.posteriorNu_nonneg line 122
  26. lemma OAI.ThreeState.posteriorMu_sq_le line 124
  27. lemma OAI.ThreeState.posteriorEta_upper line 128
  28. lemma OAI.ThreeState.integrable_messageA line 141
  29. lemma OAI.ThreeState.integrable_messageQ line 148
  30. lemma OAI.ThreeState.integral_messageA line 155
  31. lemma OAI.ThreeState.integral_messageQ line 167
  32. lemma OAI.ThreeState.positive_moment_estimates line 185