OAI/Probability/InvariantIsing/Cavity/CavityMatrixResolventBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The smooth resolvent path of a compressed finite-alphabet matrix. Its norm bounds depend on the alphabet mass, not on the number of cascade levels.

  1. def OAI.InvariantIsing.cavitySpectralMatrixPath line 16
  2. def OAI.InvariantIsing.cavitySpectralMatrixDensity line 22
  3. lemma OAI.InvariantIsing.cavity_conjugate_diagonal_norm line 30
  4. lemma OAI.InvariantIsing.cavitySpectralMatrixPath_zero line 36
  5. theorem OAI.InvariantIsing.cavitySpectralMatrixPath_lipschitz line 41
  6. theorem OAI.InvariantIsing.cavitySpectralMatrixDensity_norm_le line 54
  7. theorem OAI.InvariantIsing.hasDerivAt_cavitySpectralMatrixPath line 64
  8. theorem OAI.InvariantIsing.cavitySpectralMatrixPath_pos_eq line 81