OAI/Probability/SKRatio/Calculus/Interaction.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatio.Calculus.Interaction line 11
  2. def OAI.SKRatio.Calculus.spin line 13
  3. def OAI.SKRatio.Calculus.replace line 15
  4. def OAI.SKRatio.Calculus.halfDiff line 18
  5. def OAI.SKRatio.Calculus.field line 21
  6. def OAI.SKRatio.Calculus.mean line 24
  7. def OAI.SKRatio.Calculus.generator line 27
  8. def OAI.SKRatio.Calculus.gradientGenerator line 30
  9. theorem OAI.SKRatio.Calculus.replace_same line 37
  10. theorem OAI.SKRatio.Calculus.replace_replace line 41
  11. theorem OAI.SKRatio.Calculus.replace_self line 45
  12. theorem OAI.SKRatio.Calculus.replace_comm line 49
  13. theorem OAI.SKRatio.Calculus.halfDiff_replace line 53
  14. theorem OAI.SKRatio.Calculus.halfDiff_self line 57
  15. theorem OAI.SKRatio.Calculus.halfDiff_mul line 61
  16. theorem OAI.SKRatio.Calculus.halfDiff_comm line 74
  17. theorem OAI.SKRatio.Calculus.halfDiff_const line 84
  18. theorem OAI.SKRatio.Calculus.halfDiff_sub line 88
  19. theorem OAI.SKRatio.Calculus.halfDiff_sum line 93
  20. theorem OAI.SKRatio.Calculus.halfDiff_spin line 98
  21. theorem OAI.SKRatio.Calculus.halfDiff_generator line 105
  22. abbrev OAI.SKRatio.Calculus.Observables line 121
  23. abbrev OAI.SKRatio.Calculus.VectorFields line 122
  24. def OAI.SKRatio.Calculus.gradientLM line 124
  25. def OAI.SKRatio.Calculus.generatorLM line 135
  26. def OAI.SKRatio.Calculus.generatorCLM line 151
  27. def OAI.SKRatio.Calculus.semigroup line 154
  28. lemma OAI.SKRatio.Calculus.spin_sq line 157
  29. lemma OAI.SKRatio.Calculus.generator_mul line 160
  30. lemma OAI.SKRatio.Calculus.semigroup_hasDerivAt line 170
  31. lemma OAI.SKRatio.Calculus.semigroup_hasDerivAt' line 175
  32. lemma OAI.SKRatio.Calculus.semigroup_apply_hasDerivAt line 180
  33. lemma OAI.SKRatio.Calculus.semigroup_apply_hasDerivAt' line 186
  34. lemma OAI.SKRatio.Calculus.semigroup_continuous line 192
  35. lemma OAI.SKRatio.Calculus.semigroup_zero line 198
  36. def OAI.SKRatio.Calculus.jumpEnergy line 201
  37. lemma OAI.SKRatio.Calculus.generator_square line 204
  38. lemma OAI.SKRatio.Calculus.spin_flip_self line 210
  39. lemma OAI.SKRatio.Calculus.spin_flip line 214
  40. lemma OAI.SKRatio.Calculus.field_flip line 220
  41. lemma OAI.SKRatio.Calculus.hamiltonian_flip line 225
  42. lemma OAI.SKRatio.Calculus.mass_flip line 244
  43. lemma OAI.SKRatio.Calculus.exp_two_mul_one_sub_tanh line 250
  44. lemma OAI.SKRatio.Calculus.exp_neg_two_mul_one_add_tanh line 257
  45. def OAI.SKRatio.Calculus.flipRate line 262
  46. lemma OAI.SKRatio.Calculus.mass_flip_ratio line 265
  47. lemma OAI.SKRatio.Calculus.siteKernel_apply line 283
  48. lemma OAI.SKRatio.Calculus.generator_flip line 296
  49. theorem OAI.SKRatio.Calculus.generator_eq_transition line 312
  50. def OAI.SKRatio.Calculus.unweightedGradient line 331
  51. def OAI.SKRatio.Calculus.gradientWeight line 334
  52. def OAI.SKRatio.Calculus.weightedGradient line 337
  53. lemma OAI.SKRatio.Calculus.variance_density line 340
  54. lemma OAI.SKRatio.Calculus.halfDiff_flow_hasDerivAt line 347
  55. lemma OAI.SKRatio.Calculus.unweightedGradient_hasDerivAt line 355
  56. lemma OAI.SKRatio.Calculus.generator_unweightedGradient line 364
  57. lemma OAI.SKRatio.Calculus.unweightedGradient_commutator line 375