OAI/Probability/InvariantIsing/Cavity/CavityBaseHaarFactorization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact independence, in bounded-test form, of the Haar base spectral orbit and the small compression data in the concrete cavity coupling.

  1. def OAI.InvariantIsing.cavityConjugate line 14
  2. lemma OAI.InvariantIsing.continuous_cavityConjugate line 18
  3. lemma OAI.InvariantIsing.cavityConjugate_mul line 23
  4. lemma OAI.InvariantIsing.cavityPhysicalBase_reservoir_inv line 30
  5. theorem OAI.InvariantIsing.cavityBase_compression_factorization line 43