OAI/Probability/InvariantIsing/Magnetic/RestrictedPhysicalCavityHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint Haar factorization for the normalized cavity observable. Compression-dependent coefficients and the selected frame are retained inside the same normalized two-replica test.

  1. theorem OAI.InvariantIsing.restricted_physical_cavity_haar line 16