OAI/Probability/FreeIsing/Estimates/PairedFiniteField.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.log_sum_exp_le_of_le_add line 13
  2. theorem OAI.Problem367.abs_log_sum_exp_sub_le line 26
  3. def OAI.Problem367.pairedFieldWeight line 37
  4. theorem OAI.Problem367.pairedFieldWeight_pos line 40
  5. theorem OAI.Problem367.paired_field_eq line 44
  6. theorem OAI.Problem367.paired_field_difference_bound line 59
  7. theorem OAI.Problem367.paired_interaction_field_bound line 73
  8. def OAI.Problem367.pairedEnergy line 100
  9. theorem OAI.Problem367.paired_posterior_mean line 107
  10. theorem OAI.Problem367.paired_posterior_field_bound line 118
  11. theorem OAI.Problem367.finitePosterior_mean_equiv line 129
  12. theorem OAI.Problem367.paired_posterior_field_bound_equiv line 138
  13. theorem OAI.Problem367.finite_site_posterior_field_bound line 156