TensorGGExistence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construction of actual perturbed Gibbs limits satisfying spectral GG and geometry.

theorem OAI.InvariantIsing.tensorPerturbation_exists_geometric_GG_limit line 18

Source documentation

Haar and Gaussian concentration yield finite minimizers and a weak limit satisfying the vector Ghirlanda–Guerra identities.

theorem tensorPerturbation_exists_geometric_GG_limit
    (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)))
    (t : ℕ → ℝ) (ht : ∀ k, |t k| ≤ 1)
    (h : ℕ → ℕ → ℝ) (hh : ∀ k, Monotone (h k)) (h0 : ∀ k, 0 ≤ h k 0)
    (H : ℝ) (hH : ∀ k, h k n ≤ H) :
…

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