OAI/Probability/InvariantIsing/Arrays/TensorPrincipalObservables.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The direct and fresh principal Ward observables retain only the spin projection of the state. They therefore agree on every finite leaf cutoff.

  1. def OAI.InvariantIsing.tensorOffDirect line 18
  2. def OAI.InvariantIsing.tensorOffFresh line 27
  3. def OAI.InvariantIsing.tensorOffDirectCap line 34
  4. def OAI.InvariantIsing.tensorOffFreshCap line 38
  5. lemma OAI.InvariantIsing.tensorOffDirectCap_nonneg line 41
  6. lemma OAI.InvariantIsing.tensorOffFreshCap_nonneg line 46
  7. lemma OAI.InvariantIsing.offCoordinateProduct_abs_le line 51
  8. lemma OAI.InvariantIsing.offCoordinateVariation_abs_le line 59
  9. lemma OAI.InvariantIsing.tensorOffDirect_abs_le line 71
  10. lemma OAI.InvariantIsing.tensorOffFresh_abs_le line 94
  11. lemma OAI.InvariantIsing.measurable_tensorOffDirect_at line 112
  12. lemma OAI.InvariantIsing.measurable_tensorOffFresh_at line 123
  13. lemma OAI.InvariantIsing.measurable_tensorOffDirect line 133
  14. lemma OAI.InvariantIsing.measurable_tensorOffFresh line 139