OAI/Probability/InvariantIsing/Cavity/CavityDiagonalSpectralPrecision.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The precision assumptions in the rooted Gaussian calculation follow from the actual upper spectral gap when the base matrix is diagonal.

  1. lemma OAI.InvariantIsing.finiteInverse_antitone_pos line 15
  2. lemma OAI.InvariantIsing.cavitySpectralMatrixPath_diagonal_pos line 27
  3. theorem OAI.InvariantIsing.cavity_diagonal_spectral_step_precision line 47
  4. theorem OAI.InvariantIsing.cavity_diagonal_spectral_terminal_precision line 82