Gibbs conditional distributions

Definitionσ-algebra of the configuration outside a region#✓fully proved

The σ-algebra on ConfigSpace E generated by the coordinates outside Λ: the information about a configuration that is visible from outside the region Λ.

@[reducible] noncomputable def outsideSigma (Λ : Set E) : MeasurableSpace (ConfigSpace E) :=
  ⨆ e ∈ Λᶜ, MeasurableSpace.comap (ConfigSpace.eval e) inferInstance

Uses 2 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Coordinate projection of a configuration

Used byConditional distribution given the outside of a region · Outside conditional distribution is a version of the conditional probability · Disintegration in product form for the outside conditional distribution · Averaging the outside conditional distribution recovers the measure · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra · Convexity of the set of DLR states · Uniqueness of the Gibbs state · DLR state of the Ising model on \(\mathbb{Z}^d\) · Ising specification in a box · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Approximation in measure by events measurable outside every box · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · Tail event for lattice spin configurations

TheoremOutside σ-algebra is a sub-σ-algebra of the product σ-algebra#✓fully proved

The outside σ-algebra is a sub-σ-algebra of the product σ-algebra.

theorem outsideSigma_le (Λ : Set E) :
    outsideSigma Λ ≤ (inferInstance : MeasurableSpace (ConfigSpace E))

Uses 3 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · σ-algebra of the configuration outside a region

Proof usesCoordinate projection of a configuration

Used byOutside conditional distribution is a version of the conditional probability · Disintegration in product form for the outside conditional distribution · Averaging the outside conditional distribution recovers the measure · Convexity of the set of DLR states · Uniqueness of the Gibbs state · Ising specification as a Markov kernel · The plus state is a Gibbs (DLR) state · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

DefinitionConditional distribution given the outside of a region#✓fully proved

The conditional distribution of a finite measure μ on ConfigSpace E given the configuration outside Λ: a regular version of μ(· | outsideSigma Λ), namely Mathlib's condExpKernel μ (outsideSigma Λ). For a Gibbs measure this is the Gibbs specification in Λ (DLR condition).

noncomputable def gibbsConditional (μ : Measure (ConfigSpace E)) [IsFiniteMeasure μ]
    (Λ : Set E) : @Kernel (ConfigSpace E) (ConfigSpace E) (outsideSigma Λ) _ :=
  condExpKernel μ (outsideSigma Λ)

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · σ-algebra of the configuration outside a region

Used byOutside conditional distribution is a version of the conditional probability · Disintegration in product form for the outside conditional distribution · Averaging the outside conditional distribution recovers the measure · Convexity of the set of DLR states · Uniqueness of the Gibbs state · DLR state of the Ising model on \(\mathbb{Z}^d\) · The plus state is a Gibbs (DLR) state

TheoremAveraging the outside conditional distribution recovers the measure#✓fully proved

Disintegration: averaging the conditional distribution over μ gives back μ.

theorem gibbsConditional_comp_trim
    (μ : Measure (ConfigSpace E)) [IsFiniteMeasure μ] (Λ : Set E) :
    gibbsConditional μ Λ ∘ₘ μ.trim (outsideSigma_le Λ) = μ

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Conditional distribution given the outside of a region · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra

TheoremDisintegration in product form for the outside conditional distribution#✓fully proved

Disintegration in product form: μ.trim ⊗ₘ gibbsConditional μ Λ is the law of (ω, ω).

theorem gibbsConditional_compProd_trim
    (μ : Measure (ConfigSpace E)) [IsFiniteMeasure μ] (Λ : Set E) :
    (μ.trim (outsideSigma_le Λ)) ⊗ₘ (gibbsConditional μ Λ)
      = @Measure.map (ConfigSpace E) (ConfigSpace E × ConfigSpace E) _
          ((outsideSigma Λ).prod inferInstance) (fun ω ↦ (id ω, id ω)) μ

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Conditional distribution given the outside of a region · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra

Used byConvexity of the set of DLR states · The plus state is a Gibbs (DLR) state

TheoremOutside conditional distribution is a version of the conditional probability#✓fully proved

gibbsConditional μ Λ is a version of the conditional probability μ⟦s | outsideSigma Λ⟧.

theorem gibbsConditional_ae_eq_condExp
    (μ : Measure (ConfigSpace E)) [IsFiniteMeasure μ] (Λ : Set E)
    {s : Set (ConfigSpace E)} (hs : MeasurableSet s) :
    (fun ω ↦ ((gibbsConditional μ Λ) ω).real s) =ᵐ[μ] μ⟦s | outsideSigma Λ⟧

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Conditional distribution given the outside of a region · σ-algebra of the configuration outside a region

Proof usesOutside σ-algebra is a sub-σ-algebra of the product σ-algebra

Used byUniqueness of the Gibbs state

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.