OAI/Probability/InvariantIsing/Cavity/CavityCoupledOverlap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual spectral-image coupling gives one base eigenbasis for the interaction, the special frame, and all spectral overlaps.

  1. theorem OAI.InvariantIsing.cavity_coupled_spectral_overlap line 13