OAI/Probability/InvariantIsing/Cavity/CavityLabeledProjectors.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Joint labeled spectral projectors and special axes of the physical base model. Labels are retained even for repeated spectral values.

  1. abbrev OAI.InvariantIsing.CavityProjectorFrame line 15
  2. def OAI.InvariantIsing.cavityLabeledProjectorAction line 18
  3. lemma OAI.InvariantIsing.continuous_cavityLabeledProjectorAction line 22
  4. lemma OAI.InvariantIsing.cavityLabeledProjectorAction_mul line 32
  5. def OAI.InvariantIsing.cavityPhysicalLabeledProjectors line 41
  6. def OAI.InvariantIsing.cavityCanonicalProjectorFrame line 49
  7. lemma OAI.InvariantIsing.measurable_cavityPhysicalLabeledProjectors line 56
  8. lemma OAI.InvariantIsing.cavityPhysicalLabeledProjectors_reservoir line 69
  9. theorem OAI.InvariantIsing.cavityPhysicalLabeledProjectors_mem_orbit line 86