OAI/Probability/ClassicalON/PinnedBonds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.pinNormalization line 13
  2. theorem OAI.ClassicalON.pinNormalization_pos line 16
  3. theorem OAI.ClassicalON.sum_prescribed_bondSignProduct line 20
  4. theorem OAI.ClassicalON.integral_pole_spinBondWeight_card line 44
  5. theorem OAI.ClassicalON.prescribed_positive_card line 79
  6. theorem OAI.ClassicalON.integral_positive_spinBondWeight line 84
  7. theorem OAI.ClassicalON.integral_layer_spinBondWeight line 94
  8. def OAI.ClassicalON.poleBondMean line 106
  9. theorem OAI.ClassicalON.integral_spinWeight_sum line 111
  10. theorem OAI.ClassicalON.positive_Z line 122
  11. theorem OAI.ClassicalON.layer_Z line 134
  12. theorem OAI.ClassicalON.poleBondMean_eq_pinnedBondMean line 148