Weak and monotone limits on configuration space

DefinitionWeak convergence of probability measures on configuration space#✓fully proved

Weak convergence of a sequence of probability measures on ConfigSpace E: convergence in the topology of ProbabilityMeasure (ConfigSpace E), whose open sets are generated by the integrals of bounded continuous functions.

def WeakConvergesTo (μ : ℕ → ProbabilityMeasure (ConfigSpace E))
    (ν : ProbabilityMeasure (ConfigSpace E)) : Prop :=
  Tendsto μ atTop (𝓝 ν)

Uses 1 · Used by 47

Statement usesConfiguration space of a statistical-mechanics model

Used byPositive planar percolation at some \(p < 1\) via the Ising model · Stochastic domination from below passes to weak limits · Weak limit of a decreasing chain is dominated by its terms · Weak limit of an increasing chain dominates its terms · Lower bounds on clopen-event probabilities pass to weak limits · Upper bounds on clopen-event probabilities pass to weak limits · Weak convergence implies convergence of integrals · Portmanteau theorem for clopen events · Convergence on clopen events implies weak convergence · Convergence of integrals implies weak convergence · Stochastic domination from above passes to weak limits · Existence of infinite-volume states · Uniqueness of the Gibbs state · Infinite-volume state of a sequence of measures · The plus state is a Gibbs (DLR) state · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Peierls' theorem · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Free infinite-volume measure is a subsequential weak limit · Wired infinite-volume measure is a subsequential weak limit · Free translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Common subsequence with free and wired weak limits · Ordered free and wired subsequential limits exist for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Wired infinite-volume probability equals the infimum over boxes · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Per-box uniqueness of the random-cluster measures off a countable set · Translation invariance of the free FK measure from cylinder decay · Translation invariance of the wired FK measure from cylinder decay · Free translation invariance from decay on a dense set · Wired translation invariance from decay on a dense set · Free translation invariance from integral shift decay · Wired translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

TheoremWeak convergence implies convergence of integrals#✓fully proved

Under weak convergence, the integral of every bounded continuous function converges.

theorem WeakConvergesTo.tendsto_integral
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν) (f : (ConfigSpace E) →ᵇ ℝ) :
    Tendsto (fun n => ∫ x, f x ∂(μ n : Measure (ConfigSpace E))) atTop
      (𝓝 (∫ x, f x ∂(ν : Measure (ConfigSpace E))))

Uses 2 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Weak convergence of probability measures on configuration space

Used byPositive planar percolation at some \(p < 1\) via the Ising model · The plus state is a Gibbs (DLR) state · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Peierls' theorem · Translation invariance of the plus state · Free translation invariance from integral shift decay · Wired translation invariance from integral shift decay · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

TheoremConvergence of integrals implies weak convergence#✓fully proved

If the integral of every bounded continuous function converges, the measures converge weakly.

theorem weakConvergesTo_of_forall_tendsto_integral
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    (h : ∀ f : (ConfigSpace E) →ᵇ ℝ,
        Tendsto (fun n => ∫ x, f x ∂(μ n : Measure (ConfigSpace E))) atTop
          (𝓝 (∫ x, f x ∂(ν : Measure (ConfigSpace E))))) :
    WeakConvergesTo μ ν

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Weak convergence of probability measures on configuration space

Used byTranslation invariance of the plus state · Free translation invariance from integral shift decay · Wired translation invariance from integral shift decay

TheoremCylinder events are clopen#✓fully proved

A cylinder event of ConfigSpace E, determined by finitely many coordinates, is clopen.

theorem isClopen_cylinderEvent (s : Finset E) (S : Set (∀ _i : s, Bool)) :
    IsClopen (cylinder (α := fun _ : E => Bool) s S)

Used by 1

Used byProbability measures agreeing on clopen sets are equal

TheoremPortmanteau theorem for clopen events#✓fully proved

Under weak convergence on ConfigSpace E, the probability of every clopen event converges (portmanteau theorem).

theorem WeakConvergesTo.tendsto_real_of_isClopen
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν) {A : Set (ConfigSpace E)} (hA : IsClopen A) :
    Tendsto (fun n => (μ n : Measure (ConfigSpace E)).real A) atTop
      (𝓝 ((ν : Measure (ConfigSpace E)).real A))

Uses 2 · Used by 17

Statement usesConfiguration space of a statistical-mechanics model · Weak convergence of probability measures on configuration space

Used byWeak limit of a decreasing chain is dominated by its terms · Weak limit of an increasing chain dominates its terms · Lower bounds on clopen-event probabilities pass to weak limits · Upper bounds on clopen-event probabilities pass to weak limits · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Wired percolation bound \(\theta^1(p, q) \le (2dp)^m\) for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Wired infinite-volume probability equals the infimum over boxes · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Per-box uniqueness of the random-cluster measures off a countable set · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

TheoremIncreasing-event probabilities along an increasing chain are monotone#✓fully proved

Along a chain μ₀ ≼ μ₁ ≼ ⋯, the probability of an increasing event is monotone.

theorem monotone_real_of_chain
    {μ : ℕ → Measure (ConfigSpace E)}
    (hchain : ∀ n, μ n ≼ μ (n + 1))
    (hfinite : ∀ n, IsFiniteMeasure (μ n))
    {A : Set (ConfigSpace E)} (hAmeas : MeasurableSet A) (hAinc : IsIncreasing A) :
    Monotone (fun n => (μ n).real A)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations

Proof usesStochastic domination compares real-valued masses

Used byWeak limit of an increasing chain dominates its terms

TheoremIncreasing-event probabilities along a decreasing chain are antitone#✓fully proved

Along a chain ⋯ ≼ μ₁ ≼ μ₀, the probability of an increasing event is antitone.

theorem antitone_real_of_chain
    {μ : ℕ → Measure (ConfigSpace E)}
    (hchain : ∀ n, μ (n + 1) ≼ μ n)
    (hfinite : ∀ n, IsFiniteMeasure (μ n))
    {A : Set (ConfigSpace E)} (hAmeas : MeasurableSet A) (hAinc : IsIncreasing A) :
    Antitone (fun n => (μ n).real A)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations

Proof usesStochastic domination compares real-valued masses

Used byWeak limit of a decreasing chain is dominated by its terms

TheoremWeak limit of an increasing chain dominates its terms#✓fully proved

The weak limit of an increasing chain gives each increasing clopen event at least the probability any term of the chain gives it.

theorem WeakConvergesTo.le_real_of_monotone_isIncreasing
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν)
    (hchain : ∀ n, (μ n : Measure (ConfigSpace E)) ≼ (μ (n + 1) : Measure (ConfigSpace E)))
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) (n : ℕ) :
    (μ n : Measure (ConfigSpace E)).real A ≤ (ν : Measure (ConfigSpace E)).real A

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations · Weak convergence of probability measures on configuration space

Proof usesPortmanteau theorem for clopen events · Increasing-event probabilities along an increasing chain are monotone

TheoremWeak limit of a decreasing chain is dominated by its terms#✓fully proved

The weak limit of a decreasing chain gives each increasing clopen event at most the probability any term of the chain gives it.

theorem WeakConvergesTo.ge_real_of_antitone_isIncreasing
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν)
    (hchain : ∀ n, (μ (n + 1) : Measure (ConfigSpace E)) ≼ (μ n : Measure (ConfigSpace E)))
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) (n : ℕ) :
    (ν : Measure (ConfigSpace E)).real A ≤ (μ n : Measure (ConfigSpace E)).real A

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations · Weak convergence of probability measures on configuration space

Proof usesPortmanteau theorem for clopen events · Increasing-event probabilities along a decreasing chain are antitone

TheoremLower bounds on clopen-event probabilities pass to weak limits#✓fully proved

A lower bound on the probabilities of a clopen event along a weakly convergent sequence passes to the limit.

theorem le_real_of_weakLimit
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    {ρ : Measure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν)
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (_hAinc : IsIncreasing A)
    (hbound : ∀ n, ρ.real A ≤ (μ n : Measure (ConfigSpace E)).real A) :
    ρ.real A ≤ (ν : Measure (ConfigSpace E)).real A

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Weak convergence of probability measures on configuration space

Proof usesPortmanteau theorem for clopen events

Used byStochastic domination from below passes to weak limits

TheoremUpper bounds on clopen-event probabilities pass to weak limits#✓fully proved

An upper bound on the probabilities of a clopen event along a weakly convergent sequence passes to the limit.

theorem real_le_of_weakLimit
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    {ρ : Measure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν)
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A)
    (hbound : ∀ n, (μ n : Measure (ConfigSpace E)).real A ≤ ρ.real A) :
    (ν : Measure (ConfigSpace E)).real A ≤ ρ.real A

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Weak convergence of probability measures on configuration space

Proof usesPortmanteau theorem for clopen events

Used byStochastic domination from above passes to weak limits

TheoremStochastic domination from below passes to weak limits#✓fully proved

If ρ ≼ μₙ for all n and μₙ → ν weakly, then ρ(A) ≤ ν(A) for every increasing clopen event A.

theorem dominated_weakLimit_of_forall_dominated
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    {ρ : Measure (ConfigSpace E)}
    (h : WeakConvergesTo μ ν)
    (hdom : ∀ n, ρ ≼ (μ n : Measure (ConfigSpace E)))
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) :
    ρ.real A ≤ (ν : Measure (ConfigSpace E)).real A

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations · Weak convergence of probability measures on configuration space

Proof usesStochastic domination compares real-valued masses · Lower bounds on clopen-event probabilities pass to weak limits

TheoremStochastic domination from above passes to weak limits#✓fully proved

If μₙ ≼ ρ for all n and μₙ → ν weakly, then ν(A) ≤ ρ(A) for every increasing clopen event A.

theorem weakLimit_dominated_of_forall_dominated
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {ν : ProbabilityMeasure (ConfigSpace E)}
    {ρ : Measure (ConfigSpace E)} [IsFiniteMeasure ρ]
    (h : WeakConvergesTo μ ν)
    (hdom : ∀ n, (μ n : Measure (ConfigSpace E)) ≼ ρ)
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) :
    (ν : Measure (ConfigSpace E)).real A ≤ ρ.real A

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations · Weak convergence of probability measures on configuration space

Proof usesStochastic domination compares real-valued masses · Upper bounds on clopen-event probabilities pass to weak limits

TheoremProbability measures agreeing on clopen sets are equal#✓fully proved

Two probability measures on ConfigSpace E that agree on clopen sets are equal: the clopen cylinder events form a generating π-system.

theorem ProbabilityMeasure.ext_of_forall_isClopen
    {μ ν : ProbabilityMeasure (ConfigSpace E)}
    (h : ∀ A : Set (ConfigSpace E), IsClopen A → μ A = ν A) : μ = ν

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Proof usesCylinder events are clopen

Used byConvergence on clopen events implies weak convergence

TheoremSubsequential weak limits are determined by clopen-event limits#✓fully proved

If the probabilities of clopen events converge to L, every subsequential weak limit ξ satisfies ξ(A) = L(A) on clopen A.

theorem isClopen_apply_eq_of_subseq_tendsto
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {L : Set (ConfigSpace E) → NNReal}
    (hconv : ∀ A : Set (ConfigSpace E), IsClopen A → Tendsto (fun n => (μ n) A) atTop (𝓝 (L A)))
    {ξ : ProbabilityMeasure (ConfigSpace E)} {ψ : ℕ → ℕ} (hψ : StrictMono ψ)
    (htends : Tendsto (μ ∘ ψ) atTop (𝓝 ξ))
    {A : Set (ConfigSpace E)} (hA : IsClopen A) :
    (ξ A : NNReal) = L A

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byConvergence on clopen events implies weak convergence

TheoremConvergence on clopen events implies weak convergence#✓fully proved

If the probability of every clopen event converges along a sequence of probability measures on ConfigSpace E, the sequence converges weakly: all subsequential limits (which exist by Prokhorov) agree on clopen sets, hence coincide.

theorem tendsto_weakly_of_forall_isClopen_tendsto
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)} {L : Set (ConfigSpace E) → NNReal}
    (hconv : ∀ A : Set (ConfigSpace E), IsClopen A → Tendsto (fun n => (μ n) A) atTop (𝓝 (L A))) :
    ∃ ν : ProbabilityMeasure (ConfigSpace E), WeakConvergesTo μ ν

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Weak convergence of probability measures on configuration space

Proof usesProbability measures agreeing on clopen sets are equal · Subsequential weak limits are determined by clopen-event limits

TheoremConvergence of increasing-event probabilities along an increasing chain#✓fully proved

Along a chain μ₀ ≼ μ₁ ≼ ⋯, the probability of an increasing clopen event converges to its supremum.

theorem tendsto_NNReal_of_monotone_isIncreasing
    {μ : ℕ → ProbabilityMeasure (ConfigSpace E)}
    (hchain : ∀ n, (μ n : Measure (ConfigSpace E)) ≼ (μ (n + 1) : Measure (ConfigSpace E)))
    {A : Set (ConfigSpace E)} (hAclopen : IsClopen A) (hAinc : IsIncreasing A) :
    Tendsto (fun n => (μ n) A) atTop (𝓝 (⨆ n, (μ n) A))

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations

Proof usesStochastic domination compares real-valued masses

Used byConvergence to the free two-point function under stochastic increase

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.