SpinPriorArrayLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-replica tests of the actual tensor spectral-array law.

def OAI.InvariantIsing.spinPriorArrayLaw line 15

theorem OAI.InvariantIsing.spinPriorArrayLaw_test line 28

Source documentation

Injection into the infinite replica sequence gives the exact actual finite-replica mean, while retaining its common rotation.

theorem spinPriorArrayLaw_test {N m k z : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (π : Measure (Spin N)) [IsProbabilityMeasure π] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (r : Fin k → ℕ) (h : ℕ → ℝ)
    (F : SpectralArray (m + 1) → ℝ) (hF : Continuous F)
    (D : SpecialOrthogonal N → (Fin z → Spin N × LabeledLeaf n) → ℝ)
    (ι : Fin z → ℕ) (hi : Function.Injective ι)
    (he : ∀ (U : SpecialOrthogonal N) (σ : ℕ → Spin N × LabeledLeaf n), F (fun ij : ℕ × ℕ =>
      spectralJointEntry (specialRotation U) I n (σ ij.1) (σ ij.2)) = D U (fun i => σ (ι i))) :
    (∫ x, F x ∂(spinPriorArrayLaw μ π eig c I degree amplitude n b r h :
      Measure (SpectralArray (m + 1)))) =
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.spectralJointEntry, OAI.InvariantIsing.specialRotation, OAI.InvariantIsing.spinPriorArrayLaw