OAI/Probability/InvariantIsing/Arrays/TensorDiagonalWardLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantIsing.tensorNamespacedArrayLaw_diagonalWard_limit line 16
2. theorem OAI.InvariantIsing.tensorNamespacedArrayLaw_diagonalWard_equation line 50

   Source documentation

   Under the independently proved constant limiting diagonals, the actual diagonal Ward equation has the manuscript's projected-product form.

   theorem tensorNamespacedArrayLaw_diagonalWard_equation {m : ℕ}
       (Q : ProbabilityMeasure (SpectralArray (m + 1))) (ρ eig : Fin m → ℝ) (a b : Fin m)
       (q : Fin (m + 1) → ℝ)
       (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), ∀ i j, (x (i,i) j : ℝ) = q j)
       (hward : spectralDiagonalWardResidual Q ρ eig a b = 0) :
       ρ b * q a.castSucc - ρ a * q b.castSucc =
         (eig a - eig b) * (q a.castSucc * q b.castSucc -
           ∫ x, (x (0,1) a.castSucc : ℝ) * (x (0,1) b.castSucc : ℝ)
             ∂(Q : Measure (SpectralArray (m + 1)))) := by
   …

   Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.spectralDiagonalWardResidual