OAI/Probability/InvariantIsing/Fields/PriorTemperatureModulus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Temperature continuity for the actual fixed-prior pressure. The spectral perturbation is held fixed while the original interaction scales.

  1. theorem OAI.InvariantIsing.priorPerturbationPressureMean_temperature_modulus line 13