TensorArrayResidual.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite tensor GG residual is the spectral-array residual.

lemma OAI.InvariantIsing.spectralJointEntry_monomial line 16
lemma OAI.InvariantIsing.spectralJointEntry_selectedMonomial line 25

theorem OAI.InvariantIsing.tensorNamespacedArrayLaw_residual line 35

Source documentation

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

theorem tensorNamespacedArrayLaw_residual {N m k q : ℕ}
    (μ : Measure (SpecialOrthogonal 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 : ℕ → ℝ) (j : Fin k)
    (e : Equiv.Perm (Fin (q + 1))) (D : SpectralBlock (m + 1) (q + 1) → ℝ) (hD : Continuous D) :
    spectralMonomialResidual (tensorNamespacedArrayLaw μ eig c I degree amplitude n b r h)
      (q + 1) (e 0) D (Fin.lastCases (r j) (degree j)) =
      tensorSpectralGGResidual μ eig c I degree amplitude n b r h j
        (permutedSpectralBlockTest I n e D) := by
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpectralBlock, OAI.InvariantIsing.spectralMonomialResidual, OAI.InvariantIsing.tensorNamespacedArrayLaw, OAI.InvariantIsing.tensorSpectralGGResidual, OAI.InvariantIsing.permutedSpectralBlockTest