OAI/Probability/InvariantIsing/Cavity/CavityRotationArray.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The spectral array of the concrete base rotation/Gaussian Gibbs law. The same rotation supplies its overlaps and cavity coordinates.

  1. lemma OAI.InvariantIsing.measurable_cavityProjectedOverlap line 15
  2. lemma OAI.InvariantIsing.measurable_cavitySpectralJointEntry line 24
  3. def OAI.InvariantIsing.cavityRotationEntry line 35
  4. lemma OAI.InvariantIsing.measurable_cavityRotationEntry line 40
  5. lemma OAI.InvariantIsing.cavityRotationEntry_gram line 45
  6. def OAI.InvariantIsing.cavityRotationArrayLaw line 59
  7. lemma OAI.InvariantIsing.cavityRotationArrayLaw_gram line 71