SpectralDiagonalCenters.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact deterministic centers without assuming constant finite self-overlap.

def OAI.InvariantIsing.spectralDiagonalCenter line 14
lemma OAI.InvariantIsing.spectralDiagonalCenter_mem line 16
lemma OAI.InvariantIsing.abs_sub_spectralDiagonalCenter_le line 19
lemma OAI.InvariantIsing.spectralMonomial_clipped_self_deviation_le line 34
Source documentation
Each deterministic center may be clipped to the geometrically allowed interval before taking a subsequence. The true finite self-overlap remains inside the integral and its error is no larger.
```
lemma spectralMonomial_clipped_self_deviation_le {N m : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (b : Fin m → ℝ) (σ : Spin N) :
    |(∏ a, projectedOverlap U (I a) σ σ ^ d a) -
      ∏ a, spectralDiagonalCenter (b a) ^ d a| ≤
        ∑ a, (d a : ℝ) * |projectedOverlap U (I a) σ σ - b a| := by
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.spectralDiagonalCenter