OAI/Probability/InvariantIsing/Arrays/TensorDiagonalPrincipalObservables.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The one- and two-replica principal observables for the diagonal Ward identity, with a generic spin projection for countable leaf passage.

  1. def OAI.InvariantIsing.tensorDiagonalDirect line 17
  2. def OAI.InvariantIsing.tensorDiagonalFresh line 25
  3. def OAI.InvariantIsing.tensorDiagonalDirectCap line 31
  4. def OAI.InvariantIsing.tensorDiagonalFreshCap line 34
  5. lemma OAI.InvariantIsing.tensorDiagonalDirectCap_nonneg line 37
  6. lemma OAI.InvariantIsing.tensorDiagonalFreshCap_nonneg line 42
  7. lemma OAI.InvariantIsing.tensorDiagonalDirect_abs_le line 47
  8. lemma OAI.InvariantIsing.tensorDiagonalFresh_abs_le line 66
  9. lemma OAI.InvariantIsing.measurable_tensorDiagonalDirect_at line 83
  10. lemma OAI.InvariantIsing.measurable_tensorDiagonalFresh_at line 94
  11. lemma OAI.InvariantIsing.measurable_tensorDiagonalDirect line 104
  12. lemma OAI.InvariantIsing.measurable_tensorDiagonalFresh line 109
  13. def OAI.InvariantIsing.tensorDiagonalBlockDirect line 114
  14. def OAI.InvariantIsing.tensorDiagonalBlockFresh line 119
  15. lemma OAI.InvariantIsing.tensorDiagonalDirect_eq_block line 124
  16. lemma OAI.InvariantIsing.tensorDiagonalFresh_eq_block line 161