SpinPriorArrayResidual.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact equality of the constrained finite-model and spectral-array GG residuals.

theorem OAI.InvariantIsing.spinPriorArrayLaw_residual line 15

Source documentation

Common rotation is retained in every finite test; arbitrary replica indices are handled by injective sampling, not by independence of rotations.

theorem spinPriorArrayLaw_residual {N m k n q : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (π : Measure (Spin N)) [IsProbabilityMeasure π] (b : ℕ → ℝ) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (r : Fin k → ℕ) (h : ℕ → ℝ) (j : Fin k)
    (e : Equiv.Perm (Fin (q + 1))) (D : SpectralBlock (m + 1) (q + 1) → ℝ) (hD : Continuous D) :
    spectralMonomialResidual (spinPriorArrayLaw μ π eig c I degree amplitude n b r h)
      (q + 1) (e 0) D (Fin.lastCases (r j) (degree j)) =
      spinPriorSpectralGGResidual μ π b eig c I degree amplitude r h j
        (permutedSpectralBlockTest I n e D) := by
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpectralBlock, OAI.InvariantIsing.spectralMonomialResidual, OAI.InvariantIsing.spinPriorArrayLaw, OAI.InvariantIsing.spinPriorSpectralGGResidual, OAI.InvariantIsing.permutedSpectralBlockTest