- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(\mu \in \mathfrak {M}(X,\mathcal X)\). Then, \(\pi \in \text{Ker}_{\mathcal B,\mathcal X}\) is a conditional expectation kernel for \(\mu \) if \(\mu (A\mid \mathcal B)=\pi (A\mid \cdot )\) \(\mu \)-a.e.
Let \((E,\mathcal{E})\) be a measurable space, and let \(S\) be a set. Then,
defines the cylinder events in \(\Delta \) (for each \(\Delta \in \mathcal{P}(S)\)), where each \(\text{proj}_\delta \) is the coordinate projection at coordinate \(\delta \).
Given a specification \(\gamma \), a Gibbs measures specified by \(\gamma \) is a measure \(\nu \in \mathfrak {M}(E^S, \mathcal{E}^S)\) such that \(\gamma _\Lambda (A|\cdot )\) is a conditional expectation kernel for \(\nu \) for all \(A \in \mathcal E^S\) and \(\Lambda \in \operatorname{Finset}(S)\).
A specification \(\gamma \) is independent iff
The Independent Specification with Single Spin Distribution \(\nu \) is
defines the Independent Specification with Single Spin Distribution with \(\nu \) (for each \(\nu \in \mathfrak {P}(E, \mathcal{E})\)), where \(\nu ^\Lambda \) is the usual product measure.
Let \(E\) and \(S\) be sets. Let \(\Delta \in \mathcal{P}(S)\), and let \(\omega \in E^S\). We define
to be the juxtaposition of \(\zeta \) and \(\omega \) (for each \(\zeta \in E^\Delta \)).
Let \((X,\mathcal X)\) and \((Y,\mathcal{Y})\) be measurable spaces. Then,
defines the set of kernels from \(\mathcal{Y}\) to \(\mathcal X\), where \(\mathfrak {M}(X,\mathcal X)\) is the space of measures on \(X\).
A modifier of \(\gamma \) is a family
such that the corresponding family of kernels \(\rho \gamma \) is a specification.
A family of measurable functions \(h_\Lambda : (S \to E) \to [0, \infty [\) is a premodifier if
for all \(\Lambda _1 \subseteq \Lambda _2\) and all \(\zeta , \eta : S \to E\) such that \(\zeta _{\Lambda _1^c} = \eta _{\Lambda _1^c}\).
A specification is a family of kernels \(\gamma : \operatorname{Finset}S \to \operatorname{Ker}_{\mathcal{F}_{S\setminus \Lambda }, \mathcal{E}^S}\) which is consistent, in the sense that
Let \(\mu \in \mathfrak {M}(X,\mathcal X)\) be a finite measure and let \(\pi \in \text{Ker}_{\mathcal B,\mathcal X}\) be a proper kernel. Then,
If \(\pi \in \text{Ker}_{\mathcal B, \mathcal X}\) is a conditional expectation kernel for \(\mu \), then
for all bounded \(\mathcal X\)-measurable functions \(f : X \to \mathbb R\).
If \(\pi \in \text{Ker}_{\mathcal B, \mathcal X}\) is a conditional expectation kernel for \(\mu \), then
for all \(\mathcal X\)-measurable functions \(f : X \to [0, \infty ]\).
If \(E\) is countable, \(\nu \) is the counting measure and \(\gamma \) is any specification, then
is a modifier from \(\operatorname{ISSSD}(\nu )\) to \(\gamma \).
Let \(\gamma \) be a proper specification with parameter set \(S\) and state space \((E, \mathcal{E})\), and let \(\nu \in \mathfrak {P}(E^S, \mathcal{E}^S)\). TFAE:
\(\nu \in \mathcal{G}(\gamma )\).
\(\gamma _\Lambda \circ _m\nu = \nu \) for all \(\Lambda \in \operatorname{Finset}(S)\).
\(\gamma _\Lambda \circ _m\nu = \nu \) frequently as \(\Lambda \to S\).
If \(f : X \to [0, \infty ]\) is a \(\mathcal X\)-measurable function, then \(\mu [f | \mathcal B]\) is the \(\mu \)-ae unique \(\mathcal B\)-measurable function \(X \to [0, \infty ]\) such that
for all \(B \in \mathcal B\).
If \(\rho \) is a modifier of \(\operatorname{ISSSD}(\nu ^S)\), then it is a premodifier if any of the following conditions hold:
\(E\) is countable and \(\nu \) is equivalent to the counting measure.
\(E\) is a second countable Borel space.
\(\nu \) is everywhere dense.
For all \(\Lambda _1 \subseteq \Lambda _2\) and all \(\eta : S \to E\), \(\zeta \mapsto \rho _{\Lambda _1}(\zeta \eta _{\Lambda _1^c})\) is continuous on \(E^{\Lambda _1}\).
If \(h\) is a premodifier and \(\nu \) is such that \(0 {\lt} \nu _\Lambda h_\Lambda {\lt} \infty \) for all \(\Lambda \), then
is a modifier of \(\operatorname{ISSSD}(\nu )\).
If \(\pi \) is a proper Markov kernel and \(g\) is a bounded function, then
for all \(x_0 \in X\) and functions \(f, g : X \to \mathbb R\) such that \(f\) is bounded \(\mathcal X\)-measurable and \(g\) is bounded \(\mathcal B\)-measurable.
If \(\pi \) is proper, then
for all \(x_0 \in X\) and functions \(f, g : X \to [0, \infty ]\) such that \(f\) is \(\mathcal X\)-measurable, \(g\) is \(\mathcal B\)-measurable.
If \(\rho \) is a family of measurable densities and \(\gamma \) is a proper Markov specification, then TFAE
\(\rho \) is a modifier of \(\gamma \)
For all \(\Lambda _1, \Lambda _2\) with \(\Lambda _1 \subseteq \Lambda _2\) and all \(\eta : S \to E\), we have
\[ \rho _{\Lambda _2} = \rho _{\Lambda _1}\cdot (\gamma _{\Lambda _1} \rho _{\Lambda _2}) \quad \gamma _{\Lambda _2}(\cdot |\eta )\text{-a.e.} \]
Georgii’s (1.30) is the \(\lambda \)-specification case, and assumes \(\lambda _\Lambda \rho _\Lambda =1\) from the start.
If \(\rho \) is a family of measurable densities, \(\gamma \) is a proper Markov independent specification, and \(\gamma _\Lambda (\rho _\Lambda )=1\) for all \(\Lambda \), then TFAE
\(\rho \) is a modifier of \(\gamma \)
For all \(\Lambda _1, \Lambda _2\) with \(\Lambda _1 \subseteq \Lambda _2\), \(\eta : S \to E\) and \(\gamma _{\Lambda _2 \setminus \Lambda _1}(\cdot |\alpha )\)-almost all \(\eta _2 : S \to E\), we have
\[ \rho _{\Lambda _2}(\zeta _1)\rho _{\Lambda _1}(\zeta _2) = \rho _{\Lambda _2}(\zeta _2) \rho _{\Lambda _1}(\zeta _1) \]for \(\gamma _{\Lambda _1}(\cdot |\eta _2) \times \gamma _{\Lambda _1}(\cdot |\eta _2)\)-almost all \((\zeta _1, \zeta _2)\).