OAI/Probability/FreeIsing/Posterior/FinitePosteriorVarianceInverse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FinitePosteriorVariance.spinMean line 16
  2. theorem OAI.Problem367.FinitePosteriorVariance.continuous_spinMean line 22
  3. theorem OAI.Problem367.FinitePosteriorVariance.spinMean_mem_Ioo line 27
  4. theorem OAI.Problem367.FinitePosteriorVariance.field_sub_observation_abs_le line 34
  5. theorem OAI.Problem367.FinitePosteriorVariance.field_abs_le_noise line 39
  6. theorem OAI.Problem367.FinitePosteriorVariance.measurable_field line 58
  7. theorem OAI.Problem367.FinitePosteriorVariance.integrable_exp_abs_field line 64
  8. theorem OAI.Problem367.FinitePosteriorVariance.integral_exp_abs_field_le line 74
  9. theorem OAI.Problem367.FinitePosteriorVariance.inverse_variance_pow_le_noise line 84
  10. theorem OAI.Problem367.FinitePosteriorVariance.integrable_inverse_variance_pow line 93
  11. theorem OAI.Problem367.FinitePosteriorVariance.integral_inverse_variance_pow_le line 111
  12. theorem OAI.Problem367.FinitePosteriorVariance.condExp_eq_spinMean line 128