OAI/Probability/InvariantIsing/Arrays/TensorContactRegion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The genuine compact parameter region for the finite upper comparison. Field covariance increments are nonnegative and their sum is capped.

  1. abbrev OAI.InvariantIsing.TensorContactParameter line 14
  2. def OAI.InvariantIsing.tensorContactRegion line 17
  3. lemma OAI.InvariantIsing.tensorContactRegion_bounds line 22
  4. lemma OAI.InvariantIsing.tensorContactRegion_mem line 30
  5. lemma OAI.InvariantIsing.isCompact_tensorContactRegion line 40
  6. lemma OAI.InvariantIsing.tensorContactRegion_nonempty line 44