OAI/Probability/SKGap/Terminal/SpinLocalField.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.localField line 13
  2. def OAI.SKGap.spinGradient line 15
  3. def OAI.SKGap.realSpinEnergy line 18
  4. lemma OAI.SKGap.realSpinEnergy_eq line 21
  5. lemma OAI.SKGap.dot_coupling_single line 33
  6. lemma OAI.SKGap.realSpinEnergy_update line 44
  7. lemma OAI.SKGap.spinValue_update line 59
  8. lemma OAI.SKGap.hamiltonian_update line 66
  9. lemma OAI.SKGap.localField_update_self line 72
  10. lemma OAI.SKGap.localField_update line 82
  11. def OAI.SKGap.pairBaseMass line 106
  12. def OAI.SKGap.pairMean line 109
  13. lemma OAI.SKGap.pairMean_explicit line 112
  14. lemma OAI.SKGap.pairBaseMass_nonneg line 119
  15. lemma OAI.SKGap.pairMean_mono line 127
  16. lemma OAI.SKGap.pairMean_add line 135
  17. lemma OAI.SKGap.pairMean_sub line 138
  18. lemma OAI.SKGap.pairMean_mul line 141
  19. lemma OAI.SKGap.abs_pairMean_le line 145
  20. lemma OAI.SKGap.pair_gradient_mean line 156
  21. lemma OAI.SKGap.pair_gradient_square line 162
  22. lemma OAI.SKGap.pairMean_swap line 168
  23. lemma OAI.SKGap.pair_second_gradient_square line 173
  24. lemma OAI.SKGap.pair_polynomial_cross_mean line 178