OAI/Probability/InvariantIsing/Cavity/CavityOrientation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Correcting a spectral row sign sends an orthogonal matrix to SO without changing its spectral compression blocks.

  1. def OAI.InvariantIsing.cavityOrientationSign line 14
  2. lemma OAI.InvariantIsing.cavityOrientationSign_square line 17
  3. lemma OAI.InvariantIsing.cavityOrientationSign_det line 29
  4. def OAI.InvariantIsing.cavityOrientationLift line 33
  5. lemma OAI.InvariantIsing.measurable_cavityOrientationLift line 49
  6. lemma OAI.InvariantIsing.cavityOrientationLift_right line 64
  7. lemma OAI.InvariantIsing.cavityOrientationLift_compression line 77
  8. lemma OAI.InvariantIsing.cavityOrientationLift_measure_rightInvariant line 97
  9. lemma OAI.InvariantIsing.cavityOrientationLift_compression_event line 110