OAI/Probability/InvariantIsing/Cavity/CavitySpectralTransform.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual quadratic change from the base spectral matrix to the full spectral matrix, including the derivative which transports the common root.

  1. lemma OAI.InvariantIsing.cavitySpectralMatrixDensity_posSemidef line 17
  2. lemma OAI.InvariantIsing.cavity_spectral_shift_isUnit line 30
  3. theorem OAI.InvariantIsing.cavity_spectral_transform line 52
  4. lemma OAI.InvariantIsing.cavity_spectral_tilt_isUnit line 65
  5. theorem OAI.InvariantIsing.cavity_spectral_root_transform line 85