OAI/Probability/InvariantIsing/Cavity/CavitySampledBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Spectral arrays and finite blocks sampled from the same original Gibbs configurations, with their disorder retained.

  1. def OAI.InvariantIsing.cavitySampledEntryArray line 14
  2. def OAI.InvariantIsing.cavitySampledGroupBlock line 18
  3. lemma OAI.InvariantIsing.measurable_cavitySampledEntryArray line 22
  4. lemma OAI.InvariantIsing.measurable_cavitySampledGroupBlock line 36
  5. lemma OAI.InvariantIsing.cavitySampledGroupBlock_prefix line 49
  6. lemma OAI.InvariantIsing.measurable_cavitySampledGroupVectors line 54