Overlaps.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Spectral overlap geometry

The finite projected overlaps are Gram matrices. Panchenko's ultrametricity theorem applies to their limit arrays satisfying the Ghirlanda–Guerra identities.

def OAI.InvariantIsing.projectedOverlap line 21
Source documentation
Overlap restricted to a deterministic spectral coordinate group.
```
def projectedOverlap {N : ℕ} (U : Rotation N) (I : Finset (Fin N))
    (σ τ : Spin N) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin
lemma OAI.InvariantIsing.projectedOverlap_symm line 25
lemma OAI.InvariantIsing.projectedOverlap_posSemidef line 30
Source documentation
Each spectral overlap component is a positive semidefinite Gram kernel.
```
lemma projectedOverlap_posSemidef {N m : ℕ} (U : Rotation N) (I : Finset (Fin N))
    (σ : Fin m → Spin N) :
    Matrix.PosSemidef (fun i j => projectedOverlap U I (σ i) (σ j)) := by
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap
lemma OAI.InvariantIsing.projectedOverlap_self_nonneg line 50
lemma OAI.InvariantIsing.projectedOverlap_univ line 57
Source documentation
Full spectral overlap agrees with the ordinary spin overlap, because an orthogonal rotation preserves the inner product.
```
lemma projectedOverlap_univ {N : ℕ} (U : Rotation N) (σ τ : Spin N) :
    projectedOverlap U Finset.univ σ τ =
      (N : ℝ)⁻¹ * ∑ i, spinValue (σ i) * spinValue (τ i) := by
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.spinValue

theorem OAI.InvariantIsing.ultrametric_of_gram_gg line 69

Source documentation

Panchenko (2013), Theorem 1, in the exact bounded-Gram-array specialization needed after proving GG for spectral overlap limits. The proof is already in IsingPerceptron.gg_ultrametric; GG remains an explicit hypothesis here.

theorem ultrametric_of_gram_gg {Ω : Type*} [MeasurableSpace Ω]
    {B : Ω → IsingPerceptron.RealArray} {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hB : Measurable B) (hsym : ∀ ω i j, B ω i j = B ω j i)
    (hwe : IsingPerceptron.WeaklyExchangeable B μ)
    (hgg : IsingPerceptron.HasGhirlandaGuerra B μ) {D : ℝ}
    (hgram : ∀ ω n, Matrix.PosSemidef (IsingPerceptron.arrayBlock B n ω))
    (hdiag : ∀ ω i, B ω i i = D) :
    ∀ᵐ ω ∂μ, IsingPerceptron.IsUltrametricArray (B ω) :=
…

Mentions: OAI.IsingPerceptron.RealArray, OAI.IsingPerceptron.WeaklyExchangeable, OAI.IsingPerceptron.HasGhirlandaGuerra, OAI.IsingPerceptron.arrayBlock, OAI.IsingPerceptron.IsUltrametricArray