OAI/Probability/InvariantIsing/Cavity/CavityRootedDepthMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The bounded common-depth observable disintegrated over root and forest.

  1. def OAI.InvariantIsing.cavityRootedDepthTestMean line 13
  2. lemma OAI.InvariantIsing.measurable_cavityRootedDepthTestMean line 21
  3. lemma OAI.InvariantIsing.cavityRootedDepthTest_abs_le line 31
  4. lemma OAI.InvariantIsing.cavityRootedDepthTestMean_abs_le line 37
  5. theorem OAI.InvariantIsing.cavity_rooted_depth_test_disintegration line 46
  6. theorem OAI.InvariantIsing.cavity_rooted_depth_test_product_disintegration line 66