OAI/Probability/InvariantIsing/Cavity/CavityRootedTestMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Disintegration of the bounded common-depth spin test over its actual Gaussian-root and cascade disorder.

  1. def OAI.InvariantIsing.cavityRootedSpinTestMean line 13
  2. lemma OAI.InvariantIsing.measurable_cavityRootedSpinTestMean line 21
  3. lemma OAI.InvariantIsing.cavityRootedSpinDepthTest_abs_le line 31
  4. lemma OAI.InvariantIsing.cavityRootedSpinTestMean_abs_le line 37
  5. theorem OAI.InvariantIsing.cavity_rooted_spin_test_disintegration line 46
  6. theorem OAI.InvariantIsing.cavity_rooted_spin_test_product_disintegration line 66