OAI/Probability/InvariantIsing/Cavity/CavitySlowDepth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Choosing system sizes fast enough for a prescribed sequence of finite cascade depths. Each row requires only finitely many error estimates.

  1. def OAI.InvariantIsing.cavityDiagonalIndex line 14
  2. lemma OAI.InvariantIsing.cavityDiagonalIndex_ge line 18
  3. lemma OAI.InvariantIsing.cavityDiagonalIndex_strict line 23
  4. lemma OAI.InvariantIsing.cavity_choose_diagonal_errors line 28
  5. lemma OAI.InvariantIsing.cavity_choose_depth_rates line 52