OAI/Probability/FreeIsing/Posterior/FinitePosterior.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FinitePosterior.weight line 13
  2. def OAI.Problem367.FinitePosterior.partition line 16
  3. def OAI.Problem367.FinitePosterior.mean line 19
  4. def OAI.Problem367.FinitePosterior.mass line 22
  5. lemma OAI.Problem367.FinitePosterior.weight_pos line 26
  6. lemma OAI.Problem367.FinitePosterior.partition_pos line 29
  7. lemma OAI.Problem367.FinitePosterior.partition_ne_zero line 33
  8. lemma OAI.Problem367.FinitePosterior.mass_pos line 36
  9. lemma OAI.Problem367.FinitePosterior.sum_mass line 40
  10. lemma OAI.Problem367.FinitePosterior.mean_eq_sum_mass line 46
  11. lemma OAI.Problem367.FinitePosterior.mean_const line 50
  12. lemma OAI.Problem367.FinitePosterior.hasDerivAt_weight line 55
  13. lemma OAI.Problem367.FinitePosterior.hasDerivAt_partition line 61
  14. theorem OAI.Problem367.FinitePosterior.hasDerivAt_mean line 66
  15. lemma OAI.Problem367.FinitePosterior.hasDerivAt_log_partition line 80
  16. lemma OAI.Problem367.FinitePosterior.hasDerivAt_mass line 86
  17. lemma OAI.Problem367.FinitePosterior.variance_eq_sum line 94
  18. lemma OAI.Problem367.FinitePosterior.variance_nonneg line 110
  19. lemma OAI.Problem367.FinitePosterior.variance_pos line 116
  20. theorem OAI.Problem367.FinitePosterior.hasDerivAt_spin_mean line 132
  21. theorem OAI.Problem367.FinitePosterior.mean_monotone line 143
  22. lemma OAI.Problem367.FinitePosterior.mean_lt line 152
  23. lemma OAI.Problem367.FinitePosterior.lt_mean line 163
  24. theorem OAI.Problem367.FinitePosterior.spin_mean_mem_Ioo line 174