OAI/Probability/FreeIsing/Estimates/InhomogeneousSpinChain.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.InhomogeneousChain.weight line 16
  2. theorem OAI.Problem367.InhomogeneousChain.weight_zero line 21
  3. theorem OAI.Problem367.InhomogeneousChain.weight_cons line 24
  4. theorem OAI.Problem367.InhomogeneousChain.weight_eq_prod line 30
  5. theorem OAI.Problem367.InhomogeneousChain.weight_nonneg line 40
  6. def OAI.Problem367.InhomogeneousChain.jointWeight line 46
  7. theorem OAI.Problem367.InhomogeneousChain.jointWeight_cons line 50
  8. theorem OAI.Problem367.InhomogeneousChain.jointWeight_nonneg line 56
  9. def OAI.Problem367.InhomogeneousChain.expectation line 63
  10. theorem OAI.Problem367.InhomogeneousChain.expectation_zero line 66
  11. theorem OAI.Problem367.InhomogeneousChain.expectation_succ line 70
  12. theorem OAI.Problem367.InhomogeneousChain.sum_weight line 77
  13. theorem OAI.Problem367.InhomogeneousChain.sum_jointWeight line 88
  14. theorem OAI.Problem367.InhomogeneousChain.sum_jointWeight_endpoints line 95
  15. theorem OAI.Problem367.InhomogeneousChain.expectation_affine line 108
  16. theorem OAI.Problem367.InhomogeneousChain.covariance_eq_variance_mul_prod line 141
  17. def OAI.Problem367.PosteriorChain.transition line 178
  18. theorem OAI.Problem367.PosteriorChain.transition_sum line 181
  19. theorem OAI.Problem367.PosteriorChain.transition_spinMean line 187
  20. theorem OAI.Problem367.PosteriorChain.transition_pos line 194
  21. def OAI.Problem367.PosteriorChain.intercept line 200
  22. def OAI.Problem367.PosteriorChain.slope line 203
  23. theorem OAI.Problem367.PosteriorChain.transition_spinMean_affine line 206
  24. theorem OAI.Problem367.PosteriorChain.slope_eq_responseAttenuation line 213
  25. theorem OAI.Problem367.PosteriorChain.slope_mem_Icc line 218
  26. theorem OAI.Problem367.PosteriorChain.covariance_eq_response_product line 227
  27. theorem OAI.Problem367.PosteriorChain.initial_variance_mem_Icc line 248
  28. theorem OAI.Problem367.PosteriorChain.covariance_mem_Icc line 258