OAI/Probability/FreeIsing/Estimates/MessageFunction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.cavityMessage line 9
  2. lemma OAI.Problem367.hasDerivAt_artanh_interval line 12
  3. lemma OAI.Problem367.cavityMessage_argument_mem line 31
  4. lemma OAI.Problem367.hasDerivAt_cavityMessage line 38
  5. lemma OAI.Problem367.cavityMessage_zero line 48
  6. lemma OAI.Problem367.artanh_neg_of_mem line 51
  7. lemma OAI.Problem367.cavityMessage_neg line 57
  8. lemma OAI.Problem367.abs_deriv_cavityMessage_le line 62
  9. lemma OAI.Problem367.lipschitzWith_cavityMessage line 69
  10. lemma OAI.Problem367.cavityMessage_abs_le_mul line 78
  11. lemma OAI.Problem367.cavityMessage_monotone line 84
  12. lemma OAI.Problem367.cavityMessage_le_artanh line 94
  13. lemma OAI.Problem367.cavityMessage_abs_le_artanh line 100
  14. lemma OAI.Problem367.cavityMessage_abs_ge_tanh line 110