OAI/Probability/InvariantIsing/Cavity/CavitySimultaneousFrame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single physical eigenframe represents every assignment of the spectral values. In particular it retains the labeled spectral projectors even when two physical eigenvalues coincide.

  1. theorem OAI.InvariantIsing.cavityBaseFrame_simultaneous_orbit line 15
  2. theorem OAI.InvariantIsing.cavityPhysicalBaseSpecial_simultaneous line 54