SpinPriorFiniteGG.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite constrained-prior spectral Ghirlanda–Guerra residual.

def OAI.InvariantIsing.spinPriorSpectralGGResidual line 14
lemma OAI.InvariantIsing.measurable_ggFresh line 29
Also declared: OAI/Probability/InvariantIsing/Arrays/TensorFiniteGG.lean:29 (same declaration text), OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:29 (same declaration text).
lemma OAI.InvariantIsing.measurable_ggPair line 44
Also declared: OAI/Probability/InvariantIsing/Arrays/TensorFiniteGG.lean:44 (same declaration text), OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:44 (same declaration text).
lemma OAI.InvariantIsing.measurable_ggOld line 54
Also declared: OAI/Probability/InvariantIsing/Arrays/TensorFiniteGG.lean:54 (same declaration text), OAI/Probability/InvariantIsing/Fields/PriorFiniteGG.lean:54 (same declaration text).
theorem OAI.InvariantIsing.spinPriorFiniteGG_bound line 69

theorem OAI.InvariantIsing.spinPriorFiniteGG_individualDiagonal_bound line 146

Source documentation

Each individual self-overlap error controls every selected tensor covariance. The Gaussian energy error is expressed in the same actual model.

theorem spinPriorFiniteGG_individualDiagonal_bound {N m k n q : ℕ}
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ]
    (π : Measure (Spin N)) [IsProbabilityMeasure π] (b : ℕ → ℝ) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (r : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (j : Fin k) (β e C : ℝ) (hC : 0 ≤ C) (ha : 0 < |amplitude j|)
    (D : SpecialOrthogonal N → (Fin (q + 1) → Spin N × LabeledLeaf n) → ℝ)
    (hD : Measurable (Function.uncurry D)) (hDb : ∀ U σ, |D U σ| ≤ C)
    (center δ : Fin m → ℝ)
    (hδ : ∀ a, spinPriorObservableAverage (n := n) μ π eig c I degree amplitude b r h
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinPriorObservableAverage