OAI/Probability/InvariantIsing/Cavity/CavityRotationMeasurability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability of the actual Gaussian Hamiltonian in an orthogonal eigenbasis, the disorder and the spin/leaf state.

  1. lemma OAI.InvariantIsing.measurable_cavityRotation_eval line 14
  2. lemma OAI.InvariantIsing.measurable_cavityRotation_spinTensor line 23
  3. lemma OAI.InvariantIsing.measurable_cavityRotation_perturbation line 39
  4. lemma OAI.InvariantIsing.measurable_cavityRotationHamiltonian line 49