OAI/Probability/InvariantIsing/Cavity/CavityStrictLevels.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Strict overlap levels for the finite-cascade approximation. A small convex mixture with evenly spaced interior levels removes ties and the unit top endpoint while moving every level by at most the mixture size.

  1. def OAI.InvariantIsing.cavityInteriorLevel line 14
  2. lemma OAI.InvariantIsing.cavityInteriorLevel_mem line 17
  3. lemma OAI.InvariantIsing.cavityInteriorLevel_strict line 24
  4. def OAI.InvariantIsing.cavityStrictLevels line 30
  5. lemma OAI.InvariantIsing.cavityStrictLevels_mem line 33
  6. lemma OAI.InvariantIsing.cavityStrictLevels_strict line 44
  7. lemma OAI.InvariantIsing.cavityStrictLevels_dist line 52