OAI/Probability/InvariantIsing/Fields/PriorContactMinimum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint contact minima for a fixed spin/leaf prior. The temperature scales only the original interaction, and a joint minimum supplies the actual perturbation minimum required by the constrained-prior GG construction.

  1. def OAI.InvariantIsing.priorContactObjective line 15
  2. lemma OAI.InvariantIsing.continuousOn_priorContactObjective line 23
  3. theorem OAI.InvariantIsing.priorContactObjective_exists_minimum line 43
  4. lemma OAI.InvariantIsing.priorContactObjective_eq_perturbation line 57
  5. theorem OAI.InvariantIsing.priorContact_minimum_perturbations line 67