OAI/Probability/InvariantIsing/Arrays/TensorContactMinimum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual finite joint contact minima. Restricting a joint minimum to the two perturbation boxes gives exactly the minima used in the GG limit.

  1. def OAI.InvariantIsing.tensorContactObjective line 14
  2. lemma OAI.InvariantIsing.continuousOn_tensorContactObjective line 22
  3. theorem OAI.InvariantIsing.tensorContactObjective_exists_minimum line 45
  4. lemma OAI.InvariantIsing.tensorContactObjective_eq_perturbation line 58
  5. theorem OAI.InvariantIsing.tensorContact_minimum_perturbations line 71