OAI/Probability/InvariantIsing/Arrays/BlockWard.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.coordinateWardTerm line 14
2. lemma OAI.InvariantIsing.measurable_coordinateWardTerm line 22
3. lemma OAI.InvariantIsing.abs_coordinateWardTerm_le line 33
4. lemma OAI.InvariantIsing.integrable_coordinateWardTerm line 58
5. lemma OAI.InvariantIsing.coordinateWardTerm_block_sum line 67
6. theorem OAI.InvariantIsing.block_ward_identity line 104

   Source documentation

   The exact unperturbed spectral-block rotation identity. The separate small-perturbation and limiting GG arguments are not assumed here.

   theorem block_ward_identity {N : ℕ}
       (μ : Measure (Orthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       {w : Spin N → ℝ} (hw : GibbsReference w) (eig c : Fin N → ℝ)
       (K : ℝ) (hK : 0 ≤ K) (heig : ∀ k, |eig k| ≤ K)
       (I J : Finset (Fin N)) (hIJ : Disjoint I J) (a b : ℝ)
       (hI : ∀ i ∈ I, eig i = a) (hJ : ∀ j ∈ J, eig j = b) :
       (∫ U,
         (I.card : ℝ) * gibbsAverage w (orbitHamiltonian eig c U)
           (fun σ => blockOverlap (spinCoordinate U) J σ σ) -
         (J.card : ℝ) * gibbsAverage w (orbitHamiltonian eig c U)
           (fun σ => blockOverlap (spinCoordinate U) I σ σ) +
         (a - b) *
   …

   Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.gibbsAverage, OAI.InvariantIsing.orbitHamiltonian, OAI.InvariantIsing.blockOverlap, OAI.InvariantIsing.spinCoordinate