OAI/Probability/InvariantIsing/Arrays/TensorTemperatureModulus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform temperature continuity of the enriched pressure and its identity with the pressure under the original disorder law.

  1. lemma OAI.InvariantIsing.tensorNamespacedMeanPressure_eq_disorder line 15
  2. lemma OAI.InvariantIsing.tensorNamespacedMeanPressure_eq_perturbation line 30
  3. lemma OAI.InvariantIsing.abs_tensorNamespaced_interactionEnergy_le line 40
  4. theorem OAI.InvariantIsing.tensorNamespacedMeanPressure_temperature_modulus line 67