OAI/Probability/ThreeStateClauses/PosteriorLaw.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Posterior Law.

  1. def OAI.ThreeState.TreeClauses.Experiment.messageSet line 15
  2. abbrev OAI.ThreeState.TreeClauses.Experiment.Message line 16
  3. lemma OAI.ThreeState.TreeClauses.Experiment.coordinate_nonneg line 18
  4. lemma OAI.ThreeState.TreeClauses.Experiment.coordinate_le_three line 19
  5. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_avg line 27
  6. lemma OAI.ThreeState.TreeClauses.Experiment.isClosed_messageSet line 30
  7. lemma OAI.ThreeState.TreeClauses.Experiment.isCompact_messageSet line 36
  8. instance OAI.ThreeState.TreeClauses.Experiment.(instance at line 40) line 40
  9. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_coordinate line 42
  10. lemma OAI.ThreeState.TreeClauses.Experiment.integral_avg_measure line 45
  11. lemma OAI.ThreeState.TreeClauses.Experiment.integrable_avg line 52
  12. def OAI.ThreeState.TreeClauses.Experiment.permute line 56
  13. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_permute line 63
  14. structure OAI.ThreeState.TreeClauses.Experiment.Law line 67
  15. def OAI.ThreeState.TreeClauses.Experiment.edgeMessage line 72
  16. lemma OAI.ThreeState.TreeClauses.Experiment.edge_lower line 74
  17. lemma OAI.ThreeState.TreeClauses.Experiment.edge_upper line 79
  18. lemma OAI.ThreeState.TreeClauses.Experiment.edge_positive line 84
  19. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_edgeMessage line 93
  20. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_edge_log line 98
  21. lemma OAI.ThreeState.TreeClauses.Experiment.avg_permute_vec line 112
  22. def OAI.ThreeState.TreeClauses.Experiment.permuteMeasurableEquiv line 117
  23. lemma OAI.ThreeState.TreeClauses.Experiment.compact_integrable line 125
  24. lemma OAI.ThreeState.TreeClauses.Experiment.Law.integral_equivariant line 130
  25. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_edge_centeredLog line 146
  26. lemma OAI.ThreeState.TreeClauses.Experiment.edge_permute line 151
  27. lemma OAI.ThreeState.TreeClauses.Experiment.edge_logCentered_permute line 154
  28. lemma OAI.ThreeState.TreeClauses.Experiment.Law.edge_balanced line 160
  29. lemma OAI.ThreeState.TreeClauses.Experiment.symEntropy_centeredLog' line 169
  30. lemma OAI.ThreeState.TreeClauses.Experiment.Law.edge_centeredLog_mean line 179
  31. lemma OAI.ThreeState.TreeClauses.Experiment.Law.edge_centeredLog_sq line 188
  32. def OAI.ThreeState.TreeClauses.Experiment.xMoment line 206
  33. def OAI.ThreeState.TreeClauses.Experiment.yMoment line 207
  34. lemma OAI.ThreeState.TreeClauses.Experiment.message_centered_avg line 209
  35. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_xMoment line 213
  36. lemma OAI.ThreeState.TreeClauses.Experiment.continuous_yMoment line 217
  37. lemma OAI.ThreeState.TreeClauses.Experiment.xMoment_nonneg line 221
  38. lemma OAI.ThreeState.TreeClauses.Experiment.xMoment_le_one line 223
  39. lemma OAI.ThreeState.TreeClauses.Experiment.yMoment_discriminant line 231
  40. lemma OAI.ThreeState.TreeClauses.Experiment.moment_quadratic_nonneg line 234
  41. def OAI.ThreeState.TreeClauses.Experiment.Law.mu line 243
  42. def OAI.ThreeState.TreeClauses.Experiment.Law.nu line 244
  43. def OAI.ThreeState.TreeClauses.Experiment.Law.eta line 245
  44. lemma OAI.ThreeState.TreeClauses.Experiment.Law.mu_nonneg line 247
  45. lemma OAI.ThreeState.TreeClauses.Experiment.Law.nu_nonneg line 248
  46. lemma OAI.ThreeState.TreeClauses.Experiment.Law.mu_le_one line 250
  47. lemma OAI.ThreeState.TreeClauses.Experiment.Law.second_moment_lower line 255
  48. lemma OAI.ThreeState.TreeClauses.Experiment.Law.moment_discriminant line 269