OAI/Probability/SKBarriers/SpinGlass/FiniteLaw.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SK.Analytic.FiniteLaw line 13
  2. def OAI.SK.Analytic.FiniteLaw.expect line 21
  3. def OAI.SK.Analytic.FiniteLaw.prob line 23
  4. theorem OAI.SK.Analytic.FiniteLaw.expect_nonneg line 25
  5. theorem OAI.SK.Analytic.FiniteLaw.expect_mono line 28
  6. theorem OAI.SK.Analytic.FiniteLaw.expect_const line 31
  7. theorem OAI.SK.Analytic.FiniteLaw.expect_zero line 34
  8. theorem OAI.SK.Analytic.FiniteLaw.expect_add line 36
  9. theorem OAI.SK.Analytic.FiniteLaw.expect_mul_const line 40
  10. theorem OAI.SK.Analytic.FiniteLaw.expect_const_mul line 44
  11. theorem OAI.SK.Analytic.FiniteLaw.expect_sum line 49
  12. theorem OAI.SK.Analytic.FiniteLaw.prob_nonneg line 54
  13. theorem OAI.SK.Analytic.FiniteLaw.prob_le_one line 57
  14. theorem OAI.SK.Analytic.FiniteLaw.prob_mono line 61
  15. theorem OAI.SK.Analytic.FiniteLaw.prob_true line 68
  16. theorem OAI.SK.Analytic.FiniteLaw.prob_false line 69
  17. theorem OAI.SK.Analytic.FiniteLaw.prob_not line 71
  18. theorem OAI.SK.Analytic.FiniteLaw.prob_or line 79
  19. theorem OAI.SK.Analytic.FiniteLaw.prob_exists line 87
  20. def OAI.SK.Analytic.FiniteLaw.prod line 101
  21. theorem OAI.SK.Analytic.FiniteLaw.prod_expect line 106
  22. theorem OAI.SK.Analytic.FiniteLaw.prod_expect_fst line 110
  23. theorem OAI.SK.Analytic.FiniteLaw.prod_expect_snd line 114
  24. def OAI.SK.Analytic.FiniteLaw.pi line 118
  25. theorem OAI.SK.Analytic.FiniteLaw.prob_eq_zero_of_support line 124
  26. def OAI.SK.Analytic.gibbsFiniteLaw line 135
  27. def OAI.SK.Analytic.pathFiniteLaw line 138
  28. theorem OAI.SK.Analytic.pathFiniteLaw_marginal line 144