OAI/Probability/SKRatio/Calculus/Expectation.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Fields.spinValue_true line 14
  2. lemma OAI.SKRatio.Fields.spinValue_false line 15
  3. lemma OAI.SKRatio.Fields.spinValue_not line 16
  4. lemma OAI.SKRatio.Fields.abs_tanh_lt_one line 19
  5. lemma OAI.SKRatio.Fields.sum_flip line 22
  6. def OAI.SKRatio.Fields.expectation line 25
  7. def OAI.SKRatio.Fields.variance line 28
  8. def OAI.SKRatio.Fields.conditionalExpectation line 31
  9. def OAI.SKRatio.Fields.dirichlet line 36
  10. theorem OAI.SKRatio.Fields.expectation_const line 39
  11. theorem OAI.SKRatio.Fields.expectation_add line 43
  12. theorem OAI.SKRatio.Fields.expectation_sub line 47
  13. theorem OAI.SKRatio.Fields.expectation_mul_const line 51
  14. theorem OAI.SKRatio.Fields.expectation_const_mul line 55
  15. theorem OAI.SKRatio.Fields.expectation_nonneg line 59
  16. theorem OAI.SKRatio.Fields.variance_nonneg line 63
  17. theorem OAI.SKRatio.Fields.dirichlet_nonneg line 66
  18. lemma OAI.SKRatio.Fields.conditionalExpectation_flip line 70
  19. lemma OAI.SKRatio.Fields.conditionalExpectation_idem line 76
  20. lemma OAI.SKRatio.Fields.expectation_flip_average line 86
  21. lemma OAI.SKRatio.Fields.conditionalExpectation_adjoint line 93
  22. lemma OAI.SKRatio.Fields.conditionalExpectation_mul_invariant line 107
  23. lemma OAI.SKRatio.Fields.conditionalExpectation_const line 115
  24. lemma OAI.SKRatio.Fields.expectation_conditionalExpectation line 121
  25. lemma OAI.SKRatio.Fields.expectation_projection_square line 126
  26. def OAI.SKRatio.Fields.heatBathGenerator line 140
  27. lemma OAI.SKRatio.Fields.expectation_sum line 143
  28. lemma OAI.SKRatio.Fields.heatBathGenerator_form line 149
  29. lemma OAI.SKRatio.Fields.heatBathGenerator_adjoint line 158
  30. lemma OAI.SKRatio.Fields.conditionalDifference_zero_iff line 169
  31. lemma OAI.SKRatio.Fields.flip_invariant_constant line 183
  32. lemma OAI.SKRatio.Fields.dirichlet_eq_zero_iff line 209
  33. def OAI.SKRatio.Fields.localField line 232
  34. def OAI.SKRatio.Fields.spinGradient line 234
  35. def OAI.SKRatio.Fields.realSpinEnergy line 237
  36. lemma OAI.SKRatio.Fields.realSpinEnergy_eq line 240
  37. lemma OAI.SKRatio.Fields.dot_coupling_single line 252
  38. lemma OAI.SKRatio.Fields.realSpinEnergy_update line 263
  39. lemma OAI.SKRatio.Fields.spinValue_update line 278
  40. lemma OAI.SKRatio.Fields.hamiltonian_update line 285
  41. lemma OAI.SKRatio.Fields.localField_update_self line 291
  42. lemma OAI.SKRatio.Fields.localField_update line 301
  43. lemma OAI.SKRatio.Fields.exp_spin line 315
  44. lemma OAI.SKRatio.Fields.exp_spin_product line 327
  45. def OAI.SKRatio.Fields.pairBoltzmannWeight line 335
  46. def OAI.SKRatio.Fields.pairBoltzmannMean line 337
  47. lemma OAI.SKRatio.Fields.pairBoltzmannWeight_factor line 340
  48. lemma OAI.SKRatio.Fields.pairBoltzmann_partition line 347
  49. lemma OAI.SKRatio.Fields.pairBoltzmannMean_eq line 353
  50. lemma OAI.SKRatio.Fields.pair_gradients_representation line 370
  51. lemma OAI.SKRatio.Fields.tanh_add_real line 381
  52. lemma OAI.SKRatio.Fields.tanh_pair_residual line 390
  53. lemma OAI.SKRatio.Fields.tanh_pair_variance line 407