OAI/Probability/FreeIsing/Cavity/LogOdds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.abs_cavityMessage_tanh_le line 9
2. theorem OAI.Problem367.cavityMessage_eq_half_log_cosh_ratio line 17
3. theorem OAI.Problem367.cavityMessage_eq_log_cosh_sub line 31
4. theorem OAI.Problem367.tanh_field_difference_eq line 38