OAI/Probability/FreeIsing/Cavity/BaseMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.abs_le_cosh_mul_abs_tanh line 11
  2. theorem OAI.Problem367.sq_le_tanh_sq_add_fourth line 23
  3. theorem OAI.Problem367.integrable_tanh_sq line 48
  4. theorem OAI.Problem367.integral_sq_le_tanh_sq_add_fourth line 60
  5. theorem OAI.Problem367.integral_abs_le_sqrt_integral_sq line 88
  6. theorem OAI.Problem367.integrable_abs_pow_of_bounded_perturbation line 99
  7. theorem OAI.Problem367.integrable_cavity_abs_pow_of_gaussian_bound line 117
  8. def OAI.Problem367.cavityBaseConstant line 126
  9. theorem OAI.Problem367.cavityBaseConstant_pos line 129
  10. theorem OAI.Problem367.cavity_base_second_moment line 134
  11. theorem OAI.Problem367.cavity_base_first_moment line 163