OAI/Probability/InvariantIsing/Arrays/OffDiagonalWard.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.abs_crossCoordinateProduct_le line 14
2. def OAI.InvariantIsing.offCoordinateProduct line 23
3. def OAI.InvariantIsing.offCoordinateVariation line 27
4. lemma OAI.InvariantIsing.hasDerivAt_offCoordinateProduct line 32
5. theorem OAI.InvariantIsing.offDiagonal_coordinate_ward_identity line 47

   Source documentation

   Exact finite off-diagonal rotation identity. The spin test is fixed during rotation; in the main application it is a function of the rotation-invariant total overlap. Arbitrary deterministic nonzero positive priors are allowed.

   theorem offDiagonal_coordinate_ward_identity {N : ℕ} (i j : Fin N) (hij : i ≠ j)
       (μ : Measure (Orthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       {w : Spin N → ℝ} (hw : GibbsReference w) (eig c : Fin N → ℝ)
       (F : Spin N → Spin N → ℝ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ σ τ, |F σ τ| ≤ B) :
       (∫ U,
         gibbsPairAverage w (orbitHamiltonian eig c U)
           (fun σ τ => (spinCoordinate U σ j * spinCoordinate U τ j -
             spinCoordinate U σ i * spinCoordinate U τ i) * F σ τ) +
         (eig i - eig j) *
           (gibbsPairAverage w (orbitHamiltonian eig c U)
             (fun σ τ => spinCoordinate U σ i * spinCoordinate U τ j * F σ τ *
               (coordinateProduct i j U σ + coordinateProduct i j U τ)) -
   …

   Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.gibbsPairAverage, OAI.InvariantIsing.orbitHamiltonian, OAI.InvariantIsing.spinCoordinate, OAI.InvariantIsing.coordinateProduct