OAI/Probability/InvariantIsing/Cavity/CavityProjectorHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The joint Haar law of the labeled base projectors and their special axes factors from the compression matrices. This statement keeps the information used by the actual perturbation.

  1. theorem OAI.InvariantIsing.cavity_labeled_projector_haar_factorization line 15