OAI/Probability/InvariantIsing/Cavity/CavitySplitOverlapTest.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full and retained ordinary-overlap observables differ uniformly by a vanishing amount, also under the random-tree Gibbs average.

  1. def OAI.InvariantIsing.cavityFullOverlapInsertion line 14
  2. def OAI.InvariantIsing.cavitySplitOverlapInsertion line 18
  3. theorem OAI.InvariantIsing.cavity_full_split_overlap_test_tendsto line 23
  4. theorem OAI.InvariantIsing.cavity_full_split_tree_overlap_test_tendsto line 63