OAI/Probability/InvariantIsing/Cavity/CavityBaseSpecialHaar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The joint Haar law of the actual base interaction and its special axes is independent of the cavity compression matrices.

  1. def OAI.InvariantIsing.cavityBaseSpecialAction line 15
  2. lemma OAI.InvariantIsing.continuous_cavityBaseSpecialAction line 20
  3. lemma OAI.InvariantIsing.cavityBaseSpecialAction_mul line 27
  4. theorem OAI.InvariantIsing.cavityConcreteBaseSpecial_haar_factorization line 37