OAI/Probability/InvariantIsing/Magnetic/RestrictedSpinEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual constrained spin-pair test under the finite published endpoint marking input. Integrability is proved from the full model.

  1. def OAI.InvariantIsing.restrictedFieldSpinPairIntegrand line 15
  2. def OAI.InvariantIsing.restrictedFieldSpinPairMean line 26
  3. lemma OAI.InvariantIsing.measurable_restrictedFieldSpinPairIntegrand line 30
  4. lemma OAI.InvariantIsing.restrictedFieldSpinPairIntegrand_abs_le line 55
  5. lemma OAI.InvariantIsing.measurable_restrictedFieldSpinPairMean line 66
  6. lemma OAI.InvariantIsing.restrictedFieldSpinPairMean_abs_le line 71
  7. theorem OAI.InvariantIsing.restricted_field_spin_pair_reduce line 79
  8. theorem OAI.InvariantIsing.restricted_field_spin_pair_evaluation line 92