OAI/Probability/InvariantIsing/Fields/SpinPriorCascadeAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The quenched cascade pressure is exactly the average of the fixed-leaf prior pressures. The logarithm remains inside the cascade average.

  1. lemma OAI.InvariantIsing.spinPriorMeanPressure_prior_average line 14
  2. lemma OAI.InvariantIsing.spinPriorNamespacedLog_uniform line 55
  3. lemma OAI.InvariantIsing.spinPriorMeanPressure_uniform line 62