OAI/Probability/InvariantIsing/Arrays/TensorLimitingGG.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Every weak spectral-array limit of actual finite perturbation minimizers satisfies the full vector Ghirlanda–Guerra identities.

  1. lemma OAI.InvariantIsing.enumeratedJointMonomial_surjective line 15
  2. def OAI.InvariantIsing.tensorPerturbedArrayLaw line 32
  3. theorem OAI.InvariantIsing.tensorPerturbation_minimizers_spectralGG line 42

    Source documentation

    Finite-model minimizers enforce the vector Ghirlanda–Guerra identities in every weak array limit.

    theorem tensorPerturbation_minimizers_spectralGG
    (hhaar : HaarConcentrationInput) (hgauss : GaussianLipschitzVarianceInput)
    (N : ℕ → ℕ) (hN : ∀ k, 3 ≤ N k) (hNlim : Tendsto N atTop atTop)
    (m n : ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b)
    (μ : (k : ℕ) → Measure (SpecialOrthogonal (N k))) [∀ k, IsProbabilityMeasure (μ k)]
    (hμinv : ∀ k, (μ k).IsMulLeftInvariant)
    (eig c : (k : ℕ) → Fin (N k) → ℝ) (K : ℝ) (hK : 0 < K)
    (heig : ∀ k i, |eig k i| ≤ K)
    (I : (k : ℕ) → Fin m → Finset (Fin (N k)))
    (u : (k : ℕ) → Fin (N k) → ℝ) (hu : ∀ k j, u k j ∈ Set.Icc (1 : ℝ) 2)
    (v : ℕ → Fin m → ℝ) (hv : ∀ k a, v k a ∈ Set.Icc (1 : ℝ) 2)
    (t : ℕ → ℝ) (ht : ∀ k, |t k| ≤ 1)
…

    Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal