OAI/Probability/FreeIsing/Posterior/ObservationMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.memLp_weighted_sum line 12
  2. theorem OAI.Problem367.integral_mul_weighted_sum line 17
  3. theorem OAI.Problem367.integral_weighted_sum_sq line 35
  4. theorem OAI.Problem367.integral_mul_centered_noise line 54
  5. theorem OAI.Problem367.integral_observation_mul_observation line 61
  6. theorem OAI.Problem367.integral_signal_mul_observation line 93
  7. theorem OAI.Problem367.integral_noise_mul_noise line 110
  8. theorem OAI.Problem367.integral_weighted_noise_sq line 122
  9. theorem OAI.Problem367.integral_signal_mul_weighted_observation line 142
  10. theorem OAI.Problem367.integral_weighted_observation_sq line 156
  11. theorem OAI.Problem367.centered_gaussian_moments line 181
  12. theorem OAI.Problem367.integral_weighted_gaussian_observation_sq line 192
  13. theorem OAI.Problem367.critical_information_from_spin_sums line 206