OAI/Probability/FreeIsing/Posterior/DerivativeBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.FinitePosterior.abs_mean_le line 13
  2. lemma OAI.Problem367.FinitePosterior.abs_spin_eq_one line 28
  3. theorem OAI.Problem367.FinitePosterior.abs_mean_spin_le_one line 32
  4. theorem OAI.Problem367.FinitePosterior.abs_tiltCovariance_le line 37
  5. theorem OAI.Problem367.FinitePosterior.abs_deriv_mean_le line 60
  6. theorem OAI.Problem367.FinitePosterior.abs_deriv_deriv_mean_le line 67
  7. lemma OAI.Problem367.FinitePosterior.deriv_mean_square line 80
  8. theorem OAI.Problem367.FinitePosterior.abs_deriv_mean_square_le line 87
  9. theorem OAI.Problem367.FinitePosterior.abs_deriv_deriv_mean_square_le line 101
  10. theorem OAI.Problem367.FinitePosterior.abs_fieldMean_le line 134
  11. theorem OAI.Problem367.FinitePosterior.abs_fieldCovariance_le line 141
  12. theorem OAI.Problem367.FinitePosterior.abs_fieldMean_square_le line 150
  13. theorem OAI.Problem367.FinitePosterior.abs_deriv_fieldMean_coordinate_le line 162
  14. theorem OAI.Problem367.FinitePosterior.abs_deriv_deriv_fieldMean_coordinate_le line 171
  15. theorem OAI.Problem367.FinitePosterior.abs_deriv_fieldMean_square_coordinate_le line 180
  16. theorem OAI.Problem367.FinitePosterior.abs_deriv_deriv_fieldMean_square_coordinate_le line 189