OAI/Probability/InvariantIsing/Fields/SpinPriorFrozenReference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One independent Gaussian coordinate frozen inside the actual constrained cascade model. The cascade tree remains part of the external disorder.

  1. def OAI.InvariantIsing.spinPriorFrozenReference line 12
  2. instance OAI.InvariantIsing.spinPriorFrozenReference_probability line 19
  3. lemma OAI.InvariantIsing.measurable_spinPriorFrozenReference line 26
  4. theorem OAI.InvariantIsing.spinPriorFrozenBase_exp_integrable_ae line 40