OAI/Probability/InvariantIsing/Cavity/CavityProjectorCavity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The normalized cavity observable as a measurable function of the physical labeled projectors, selected frame and small coefficient blocks.

  1. def OAI.InvariantIsing.cavityFrameCoordinates line 16
  2. lemma OAI.InvariantIsing.continuous_cavityFrameCoordinates line 20
  3. lemma OAI.InvariantIsing.measurable_cavityBlockPotential line 25
  4. def OAI.InvariantIsing.cavityProjectorCavityMean line 35
  5. lemma OAI.InvariantIsing.cavityProjectorCavityMean_bound line 46
  6. lemma OAI.InvariantIsing.measurable_cavityProjectorCavityMean line 64