OAI/Probability/SKRatio/Calculus/PairUpdate.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Fields.tanh_pair_mean line 14
  2. lemma OAI.SKRatio.Fields.pairBoltzmann_cubic_bound line 21
  3. lemma OAI.SKRatio.Fields.update_true_false line 41
  4. lemma OAI.SKRatio.Fields.conditionalExpectation_updates line 54
  5. lemma OAI.SKRatio.Fields.weight_update_factor line 65
  6. lemma OAI.SKRatio.Fields.conditionalExpectation_local line 72
  7. lemma OAI.SKRatio.Fields.spin_affine line 92
  8. lemma OAI.SKRatio.Fields.conditionalDifference_local line 102
  9. lemma OAI.SKRatio.Fields.spinGradient_update line 110
  10. lemma OAI.SKRatio.Fields.conditionalSiteEnergy_local line 114
  11. def OAI.SKRatio.Fields.pairUpdate line 127
  12. lemma OAI.SKRatio.Fields.pairUpdate_overwrite line 130
  13. lemma OAI.SKRatio.Fields.pairUpdate_left line 139
  14. lemma OAI.SKRatio.Fields.pairUpdate_right line 141
  15. lemma OAI.SKRatio.Fields.sum_spin_update line 144
  16. lemma OAI.SKRatio.Fields.sum_pairUpdate line 153
  17. def OAI.SKRatio.Fields.pairConditionalMean line 159
  18. lemma OAI.SKRatio.Fields.pairConditionalMean_update line 164
  19. lemma OAI.SKRatio.Fields.pairConditional_partition_pos line 169
  20. lemma OAI.SKRatio.Fields.expectation_pairConditionalMean line 175
  21. lemma OAI.SKRatio.Fields.pairUpdate_hamiltonian line 191
  22. lemma OAI.SKRatio.Fields.pairUpdate_localField₁ line 205
  23. lemma OAI.SKRatio.Fields.pairUpdate_localField₂ line 216
  24. lemma OAI.SKRatio.Fields.pairUpdate_gradient₁ line 224
  25. lemma OAI.SKRatio.Fields.pairUpdate_gradient₂ line 236
  26. lemma OAI.SKRatio.Fields.pairConditionalMean_boltzmann line 242
  27. def OAI.SKRatio.Fields.siteVariance line 262
  28. def OAI.SKRatio.Fields.weightedGradient line 265
  29. lemma OAI.SKRatio.Fields.expectation_mono line 268
  30. lemma OAI.SKRatio.Fields.pairConditional_cubic_bound line 274
  31. lemma OAI.SKRatio.Fields.gibbs_pair_cubic_bound line 294
  32. lemma OAI.SKRatio.Fields.siteVariance_pos line 312
  33. lemma OAI.SKRatio.Fields.siteVariance_le_one line 319
  34. lemma OAI.SKRatio.Fields.dirichlet_weighted line 322
  35. lemma OAI.SKRatio.Fields.heatBathGenerator_square line 327
  36. lemma OAI.SKRatio.Fields.positive_form_cauchy line 334
  37. lemma OAI.SKRatio.Fields.curvature_poincare_on_kernel_orthogonal line 349
  38. lemma OAI.SKRatio.Fields.conditionalExpectation_add line 372
  39. lemma OAI.SKRatio.Fields.conditionalExpectation_smul line 378
  40. def OAI.SKRatio.Fields.heatBathLinear line 385
  41. def OAI.SKRatio.Fields.gibbsScale line 401
  42. lemma OAI.SKRatio.Fields.gibbsScale_inner line 414
  43. lemma OAI.SKRatio.Fields.heatBathLinear_const line 425