SpinCorrelation.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BufferedIsing.pinExtension line 12
Source documentation
Extension by the actual common pins, in contrast to the deleted zero-field comparison graph.
```
def pinExtension {n : ℕ} (F : Finset (Fin n)) (τ : Spins n)
    (σ : KeptVertex F → Bool) : Spins n :=
…
```
Mentions: OAI.BufferedIsing.Spins, OAI.BufferedIsing.KeptVertex
lemma OAI.BufferedIsing.pinExtension_agrees line 16
lemma OAI.BufferedIsing.pinExtension_apply line 21
def OAI.BufferedIsing.pinExtensionEquiv line 28
Source documentation
Fixing sites is exactly elimination of their spin variables. This finite bijection does not replace their interactions by deletion.
```
def pinExtensionEquiv {n : ℕ} (F : Finset (Fin n)) (τ : Spins n) :
    (KeptVertex F → Bool) ≃ {σ : Spins n // AgreesOn F σ τ} where
…
```
Mentions: OAI.BufferedIsing.Spins, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.AgreesOn
lemma OAI.BufferedIsing.constrainedSum_delete_variables line 40
def OAI.BufferedIsing.pairTable line 63
Source documentation
A finite two-spin table extracted from a not necessarily normalized spin weight.
```
noncomputable def pairTable {V : Type*} [Fintype V] [DecidableEq V] (W : (V → Bool) → ℝ)
    (i j : V) (s t : Bool) : ℝ :=
…
```
lemma OAI.BufferedIsing.pairTable_sum line 67
lemma OAI.BufferedIsing.pairTable_expectation line 85
def OAI.BufferedIsing.spinFlipEquiv line 96
Source documentation
Global spin reversal is a permutation of configurations.
```
def spinFlipEquiv (V : Type*) : (V → Bool) ≃ (V → Bool) where
…
```
lemma OAI.BufferedIsing.pairTable_flip line 102
lemma OAI.BufferedIsing.symmetricTable_balanced line 113
lemma OAI.BufferedIsing.symmetricTable_correlation line 124
lemma OAI.BufferedIsing.respects_spinFlip line 131
lemma OAI.BufferedIsing.deletedEnergy_spinFlip line 136
lemma OAI.BufferedIsing.contractedZeroWeight_spinFlip line 152
lemma OAI.BufferedIsing.contractedZeroWeight_nonneg line 158
lemma OAI.BufferedIsing.contractedZero_pairTable_pos line 166
lemma OAI.BufferedIsing.qZero_eq_tanh_effective line 190
Source documentation
The FK terminal connection probability is the hyperbolic tangent of the zero-field effective coupling.
```
lemma qZero_eq_tanh_effective {n m : ℕ} (G : FiniteGraph n m)
    (I J F : Finset (Fin n)) (hIJ : Disjoint I J)
    (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J) :
    qZero G I J F i j =
      Real.tanh (tableCoupling (pairTable (contractedZeroWeight G I J F) i j)) := by
…
```
Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.KeptVertex, OAI.BufferedIsing.qZero, OAI.BufferedIsing.tableCoupling, OAI.BufferedIsing.pairTable, OAI.BufferedIsing.contractedZeroWeight
lemma OAI.BufferedIsing.artanh_qZero_eq_effective line 200