OAI/Probability/InvariantIsing/Arrays/CountableReplicaRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Leaf exhaustion for bounded replica observables of an arbitrary integrable Gibbs Hamiltonian. No Gaussian insertion remains in the Ward terms to which this lemma will be applied.

  1. lemma OAI.InvariantIsing.normalizedRestriction_prod line 16
  2. lemma OAI.InvariantIsing.referenceReplicaMean_restriction_tendsto line 27
  3. theorem OAI.InvariantIsing.expected_referenceReplicaMean_restriction_tendsto line 55