OAI/Probability/InvariantIsing/Cavity/CavityDiracAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Restoring the original random tree after proving an identity for each fixed tree, while retaining the rotation and Gaussian disorder.

  1. lemma OAI.InvariantIsing.cavity_bounded_dirac_average line 13
  2. lemma OAI.InvariantIsing.measurable_cavity_bounded_dirac_integral line 37