OAI/Probability/InvariantIsing/Fields/PriorTemperatureDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differentiation of the actual fixed-prior mean pressure. The derivative is the original interaction energy, with both perturbations held fixed.

  1. theorem OAI.InvariantIsing.hasDerivAt_priorPerturbationPressureMean_temperature line 14