OAI/Probability/InvariantIsing/Cavity/CavityFiniteSpectralEntries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Entrywise conversion of the actual finite spectral Gaussian covariances to the weighted spectral resolvent and its derivative.

  1. lemma OAI.InvariantIsing.cavity_finite_covariance_weighted_entry line 17
  2. lemma OAI.InvariantIsing.cavity_finite_root_weighted_entry line 28
  3. lemma OAI.InvariantIsing.cavity_finite_noise_weighted_entry line 50