OAI/Probability/InvariantIsing/Fields/SpinPriorCascadePressure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual cascade-enriched pressure for a deterministic spin prior. Normalized magnetization slices are allowed, while the cascade remains quenched and is averaged only after taking the logarithm.

  1. def OAI.InvariantIsing.spinPriorNamespacedLog line 16
  2. def OAI.InvariantIsing.spinPriorNamespacedReference line 23
  3. def OAI.InvariantIsing.spinPriorMeanPressure line 30
  4. lemma OAI.InvariantIsing.measurable_spinPriorNamespacedLog line 38
  5. lemma OAI.InvariantIsing.measurable_spinPriorNamespacedReference line 48
  6. instance OAI.InvariantIsing.spinPriorNamespacedReference_probability line 57
  7. lemma OAI.InvariantIsing.spinPriorDeterministicLog_abs_le line 66
  8. lemma OAI.InvariantIsing.spinPriorDeterministicLog_integrable line 90
  9. theorem OAI.InvariantIsing.spinPriorNamespacedLog_integrable line 103