OAI/Probability/FreeIsing/Posterior/VarianceInverse.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.exp_mul_abs_le_exp_add_exp_neg line 13
  2. theorem OAI.Problem367.integrable_exp_abs_of_gaussian_bound line 21
  3. theorem OAI.Problem367.integral_exp_abs_le_of_gaussian_bound line 44
  4. theorem OAI.Problem367.measurable_artanh_c939 line 79
  5. theorem OAI.Problem367.HasFreeIsingLaw.posterior_field_abs_le_noise line 85
  6. theorem OAI.Problem367.HasFreeIsingLaw.integrable_exp_abs_posterior_field line 110
  7. theorem OAI.Problem367.HasFreeIsingLaw.integral_exp_abs_posterior_field_le line 123
  8. theorem OAI.Problem367.inverse_spin_variance_eq_cosh_sq line 137
  9. theorem OAI.Problem367.cosh_le_exp_abs line 144
  10. theorem OAI.Problem367.inverse_spin_variance_pow_le_exp line 150
  11. theorem OAI.Problem367.HasFreeIsingLaw.integrable_inverse_posterior_variance_pow line 160
  12. theorem OAI.Problem367.HasFreeIsingLaw.integral_inverse_posterior_variance_pow_le line 181
  13. theorem OAI.Problem367.HasFreeIsingLaw.identDistrib_brownian_gibbs_posterior line 201
  14. theorem OAI.Problem367.HasFreeIsingLaw.brownian_gibbs_posterior_exponential_moment line 236
  15. theorem OAI.Problem367.HasFreeIsingLaw.brownian_gibbs_posterior_inverse_variance_moment line 257