OAI/Probability/InvariantIsing/Fields/CanonicalOrthogonalLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A concrete orthogonal Haar probability from the square Gaussian frame. This determines the orthogonal orbit law in the Wishart corollary.

  1. def OAI.InvariantIsing.squareFrameOrthogonal line 13
  2. lemma OAI.InvariantIsing.coe_squareFrameOrthogonal line 16
  3. lemma OAI.InvariantIsing.measurable_squareFrameOrthogonal line 22
  4. lemma OAI.InvariantIsing.squareFrameOrthogonal_mul line 34
  5. def OAI.InvariantIsing.orthogonalGaussianLeftHaar line 43
  6. instance OAI.InvariantIsing.squareFrameLaw_probability line 46
  7. instance OAI.InvariantIsing.orthogonalGaussianLeftHaar_probability line 51
  8. instance OAI.InvariantIsing.orthogonalGaussianLeftHaar_leftInvariant line 55
  9. def OAI.InvariantIsing.orthogonalGaussianHaar line 72
  10. instance OAI.InvariantIsing.orthogonalGaussianHaar_probability line 74
  11. instance OAI.InvariantIsing.orthogonalGaussianHaar_rightInvariant line 78