OAI/Probability/InvariantIsing/Arrays/TensorTruncatedDiagonalWard.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorRestrictionDiagonalObservable line 17
2. def OAI.InvariantIsing.tensorRestrictionDiagonalVariation line 21
3. def OAI.InvariantIsing.tensorRestrictionPrefix line 26
4. def OAI.InvariantIsing.tensorRestrictionPlanePrefix line 32
5. theorem OAI.InvariantIsing.tensorRestriction_diagonal_ward_prefix line 38
6. def OAI.InvariantIsing.tensorRestrictionHamiltonian line 110
7. def OAI.InvariantIsing.tensorRestrictionCovarianceDerivative line 117
8. lemma OAI.InvariantIsing.tensorRestrictionPairHamiltonian_eq line 124
9. theorem OAI.InvariantIsing.tensorRestriction_diagonal_ward line 136

   Source documentation

   The one-replica Ward equation for the actual full Gaussian coordinate law on any finite spin/leaf restriction.

   theorem tensorRestriction_diagonal_ward [Fintype S] {N m k n : ℕ} (hN : 0 < N)
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] [μ.IsMulLeftInvariant]
       {w : S → ℝ} (hw : GibbsReference w) (eig c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0) (x : S → Spin N × LabeledLeaf n)
       (i j : Fin N) (hij : i ≠ j) :
       let H := tensorRestrictionHamiltonian eig c I degree amplitude v x
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorRestrictionHamiltonian