OAI/Probability/InvariantIsing/Fields/SpinPriorContactMinimum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint contact minima for the actual cascade-enriched spin prior. The pressure averages the logarithm over the quenched cascade.

  1. def OAI.InvariantIsing.spinPriorPerturbationPressureMean line 14
  2. def OAI.InvariantIsing.spinPriorPerturbationObjective line 22
  3. def OAI.InvariantIsing.spinPriorContactObjective line 29
  4. lemma OAI.InvariantIsing.continuousOn_spinPriorContactObjective line 37
  5. theorem OAI.InvariantIsing.spinPriorContactObjective_exists_minimum line 57
  6. lemma OAI.InvariantIsing.spinPriorContactObjective_eq_perturbation line 71
  7. theorem OAI.InvariantIsing.spinPriorContact_minimum_perturbations line 81