OAI/Probability/InvariantIsing/Cavity/CavityActualDiagonal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The deterministic perturbation error under a fixed cavity-size jump, stated for the actual spectral-diagonal perturbation energy.

  1. lemma OAI.InvariantIsing.cavity_weighted_overlap_sum_abs line 15
  2. lemma OAI.InvariantIsing.cavity_weighted_overlap_sum_difference line 27
  3. theorem OAI.InvariantIsing.cavity_diagonal_perturbation_error line 40
  4. def OAI.InvariantIsing.cavityDeterministicRate line 73
  5. lemma OAI.InvariantIsing.cavityDeterministicRate_tendsto line 77