OAI/Probability/InvariantIsing/Arrays/TensorTemperatureCGF.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Temperature is a bounded deterministic tilt of the actual enriched Gibbs reference, with all Gaussian and cascade variables retained.

  1. lemma OAI.InvariantIsing.tensorTemperatureHamiltonian_affine line 15
  2. lemma OAI.InvariantIsing.measurable_tensorTemperatureObservable line 27
  3. lemma OAI.InvariantIsing.tensorTemperature_reference_fold line 37
  4. lemma OAI.InvariantIsing.tensorTemperatureCGF_eq_log_difference line 65