OAI/Probability/InvariantIsing/Arrays/CoordinateWard.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.spinCoordinate line 21

   Source documentation

   Spectral coordinate of a rotated Ising spin.

   def spinCoordinate {N : ℕ} (U : Orthogonal N) (σ : Spin N) (i : Fin N) : ℝ :=
   …

   Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin

2. def OAI.InvariantIsing.coordinateProduct line 24
3. def OAI.InvariantIsing.orbitHamiltonian line 27
4. lemma OAI.InvariantIsing.measurable_spinCoordinate line 30
5. lemma OAI.InvariantIsing.measurable_orbitHamiltonian line 40
6. lemma OAI.InvariantIsing.spinCoordinate_sq_le line 46
7. lemma OAI.InvariantIsing.abs_coordinateProduct_le line 51
8. lemma OAI.InvariantIsing.abs_coordinateSquareDifference_le line 60
9. lemma OAI.InvariantIsing.hasDerivAt_plane_coordinateProduct line 68
10. lemma OAI.InvariantIsing.gibbsAverage_const_mul line 80
11. theorem OAI.InvariantIsing.coordinate_ward_identity line 89

    Source documentation

    An exact coordinate Ward equation for every finite dimension, arbitrary nonzero positive spin prior, and deterministic magnetic field.

    theorem 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 → ℝ)
        (K : ℝ) (hK : 0 ≤ K) (heig : ∀ k, |eig k| ≤ K) :
        (∫ U,
          gibbsAverage w (orbitHamiltonian eig c U)
            (fun σ => spinCoordinate U σ j ^ 2 - spinCoordinate U σ i ^ 2) +
          (eig i - eig j) *
            (gibbsAverage w (orbitHamiltonian eig c U) (fun σ => coordinateProduct i j U σ ^ 2) -
              gibbsAverage w (orbitHamiltonian eig c U) (coordinateProduct i j U) ^ 2) ∂μ) = 0 := by
    …

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