OAI/Probability/InvariantIsing/Fields/PriorTemperatureCGF.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Temperature is a bounded tilt of the actual constrained-prior Gibbs measure. The spectral and Gaussian perturbations stay fixed under the tilt.

  1. lemma OAI.InvariantIsing.priorTemperatureHamiltonian_affine line 15
  2. lemma OAI.InvariantIsing.measurable_priorTemperatureObservable line 28
  3. lemma OAI.InvariantIsing.priorTemperature_reference_fold line 38
  4. lemma OAI.InvariantIsing.priorTemperatureCGF_eq_log_difference line 67
  5. lemma OAI.InvariantIsing.priorNamespacedLog_integrable line 99
  6. lemma OAI.InvariantIsing.priorNamespacedLog_integral line 119