SpectralReplicaProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Replica products for the actual simultaneous spectral GG limit.

def OAI.InvariantIsing.spectralSpinQuantilePath line 15
lemma OAI.InvariantIsing.spectralSpinQuantilePath_law line 22

theorem OAI.InvariantIsing.spectralPartition_replicaProductPath line 34

Source documentation

The actual spectral overlap product is represented by the manuscript product path under a single total-overlap quantile.

theorem spectralPartition_replicaProductPath {m : ℕ}
    {Q : ProbabilityMeasure (SpectralArray (m + 1))}
    (hgg : HasEntryGhirlandaGuerra (fun x i j => x (i,j)) (Q : Measure (SpectralArray (m + 1))))
    (hG : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), SpectralGram x)
    (q : Fin (m + 1) → ℝ) (hq : ∀ a, 0 ≤ q a)
    (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), ∀ i a, (x (i,i) a : ℝ) = q a)
    (hE : ∀ e : ℕ → ℕ, Function.Injective e →
      (Q : Measure (SpectralArray (m + 1))).map (permuteSpectralArray e) = Q)
    (hP : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), SpectralPartitionGeometry m x)
    (hn : ∀ᵐ x ∂(Q : Measure (SpectralArray (m + 1))), ∀ a, 0 ≤ (x (0,1) a : ℝ))
    (a b : Fin m) :
    ∃ f g : ℝ → ℝ, LipschitzWith 1 f ∧ LipschitzWith 1 g ∧
…

Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray, OAI.InvariantIsing.SpectralPartitionGeometry