OAI/Probability/InvariantIsing/Cavity/CavityProjectorTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensor features built directly from labeled spectral projectors. They give an eigenbasis-free representation of the actual Gaussian perturbation, with exactly its original covariance.

  1. abbrev OAI.InvariantIsing.CavityProjectorTensorIndex line 16
  2. def OAI.InvariantIsing.cavityProjectorMonomial line 19
  3. lemma OAI.InvariantIsing.cavityProjectorMonomial_cross line 25
  4. def OAI.InvariantIsing.cavityProjectorSpinFeature line 43
  5. lemma OAI.InvariantIsing.cavityProjectorSpinFeature_covariance line 50
  6. def OAI.InvariantIsing.cavityProjectorPerturbation line 78
  7. theorem OAI.InvariantIsing.cavityProjectorPerturbation_cross line 89