OAI/Probability/InvariantIsing/Cavity/CavityGroupCovariancePositive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the actual block covariance for all spectral groups and all fresh axes. No invertibility is needed.

  1. lemma OAI.InvariantIsing.continuous_cavityGroupReplicaCovariance line 15
  2. lemma OAI.InvariantIsing.cavityGroupReplicaCovariance_posSemidef line 28
  3. def OAI.InvariantIsing.cavitySpectralBlockCovariance line 62
  4. lemma OAI.InvariantIsing.continuous_cavitySpectralBlockCovariance line 67
  5. lemma OAI.InvariantIsing.cavitySpectralBlockCovariance_posSemidef line 72
  6. theorem OAI.InvariantIsing.cavity_spectral_frame_gaussian_test_tendsto line 86