FullPerturbationMinima.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

For the complete perturbation, both coordinate minima force the Ghirlanda–Guerra errors to vanish.

def OAI.InvariantIsing.tensorPerturbationPressureMean line 17
def OAI.InvariantIsing.diagonalMinimumCenter line 29

theorem OAI.InvariantIsing.fullPerturbationPressure_minimumGG line 35

Source documentation

For the manuscript's full finite perturbation, genuine pressure-coordinate minima give a GG residual bounded by two explicit rates tending to zero.

theorem fullPerturbationPressure_minimumGG (hhaar : HaarConcentrationInput)
    (hgauss : GaussianLipschitzVarianceInput) :
    ∃ C : ℝ, 0 < C ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N), IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ m : ℕ, ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
    ∀ I : Fin m → Finset (Fin N), ∀ u : Fin N → ℝ, (∀ j, u j ∈ Set.Icc (1 : ℝ) 2) →
    ∀ v : Fin m → ℝ, (∀ a, v a ∈ Set.Icc (1 : ℝ) 2) → ∀ t : ℝ, |t| ≤ 1 →
    ∀ n : ℕ, ∀ b : ℕ → ℝ, CascadeExponents n b →
    ∀ h : ℕ → ℝ, Monotone h → 0 ≤ h 0 → ∀ H : ℝ, h n ≤ H →
      let M := tensorPerturbationPressureMean μ eig c I (n := n) (b := b) (h := h)
…

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