OAI/Probability/InvariantIsing/Arrays/OverlapTestDiagonal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A single diagonal of finite cavity depths works for every continuous overlap test. Compactness is used only on the overlap interval.

  1. abbrev OAI.InvariantIsing.CompactOverlapTest line 14
  2. def OAI.InvariantIsing.compactOverlapTestExtension line 16
  3. lemma OAI.InvariantIsing.compactOverlapTestExtension_apply line 22
  4. lemma OAI.InvariantIsing.compact_overlap_test_difference_le line 27
  5. theorem OAI.InvariantIsing.exists_diagonal_overlap_tests line 44