OAI/Probability/InvariantIsing/Arrays/TensorPrincipalBlock.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite principal Ward observables contract exactly to projected overlap products when the two row groups have constant eigenvalues.

  1. lemma OAI.InvariantIsing.off_coordinate_difference_sum line 15
  2. lemma OAI.InvariantIsing.off_coordinate_direct_sum line 22
  3. lemma OAI.InvariantIsing.off_coordinate_fresh_sum line 34
  4. def OAI.InvariantIsing.tensorOffBlockDirect line 47
  5. def OAI.InvariantIsing.tensorOffBlockFresh line 54
  6. lemma OAI.InvariantIsing.tensorOffDirect_eq_block line 60
  7. lemma OAI.InvariantIsing.tensorOffFresh_eq_block line 89