OAI/Probability/InvariantIsing/Cavity/CavityReservoirFrame.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

An orthonormal base frame perpendicular to the physical cavity coordinates gives an orthogonal eigenbasis of the reservoir.

  1. lemma OAI.InvariantIsing.cavityBaseFrame_gram line 13
  2. lemma OAI.InvariantIsing.cavityBaseFrame_cavity_perp line 31
  3. lemma OAI.InvariantIsing.cavityBaseFrame_spectral_sum line 52
  4. def OAI.InvariantIsing.cavityReservoirRows line 62
  5. lemma OAI.InvariantIsing.cavityReservoirRows_conjugate line 66
  6. lemma OAI.InvariantIsing.cavityReservoirRows_gram line 73
  7. lemma OAI.InvariantIsing.cavityReservoirRows_orthogonal line 83
  8. lemma OAI.InvariantIsing.cavityPhysicalFrame_lastRows line 100
  9. lemma OAI.InvariantIsing.cavityPhysicalFrame_gram line 109
  10. lemma OAI.InvariantIsing.cavityReservoir_spectral_orbit line 123
  11. theorem OAI.InvariantIsing.cavityBaseReplacement_physical_orbit line 142