Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Optimality of the finite-graph moving-particle constant

Abstract

Linear occupation observables force every moving-particle constant k to satisfy one at most k times the effective conductance.

Definition 1.1 (Symmetric nonnegative conductances).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.IsConductance (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

A conductance is a nonnegative symmetric real function of two vertices. Zero weights represent absent edges. This expresses the weighted undirected graph of Chen, OctopusMoving_v3.tex, line 111, on a vertex type. The definition also allows disconnected networks and diagonal weights; diagonal pairs contribute zero to both energies.

Definition 1.2 (Exchanging two occupations).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.swap (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

A configuration assigns an element of Fin 2 to each vertex, with zero empty and one occupied. Precomposition with the transposition of x and y exchanges their occupations. When x equals y it fixes the configuration. This is the exchange defined in Chen, OctopusMoving_v3.tex, lines 116–120.

Definition 1.3 (The swap gradient).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.grad (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

The gradient is the change in a real observable f after exchanging x and y. Its sign is the value after the exchange minus the original value, as in Chen, OctopusMoving_v3.tex, line 116.

Definition 1.4 (Product Bernoulli mass).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.bernoulli (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

Multiply one factor for each vertex: α at an occupied vertex and 1 − α at an empty vertex. For α between zero and one this is the constant-density product Bernoulli probability mass of Chen, OctopusMoving_v3.tex, lines 122–123. The expression is defined for every real α.

Definition 1.5 (Expectation of an observable).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.expect (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

The dot product sums the value of f at each configuration multiplied by its Bernoulli mass. This is the finite-space version of the expectation notation introduced in Chen, OctopusMoving_v3.tex, line 128. For real α outside the probability interval the same finite weighted sum remains defined.

Definition 1.6 (The exclusion Dirichlet energy).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.exclusionEnergy (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

Sum each squared swap gradient in expectation, weighted by its conductance. The inner factor one half converts the sum over ordered vertex pairs into a sum over undirected edges. The outer factor one half is the Dirichlet-energy prefactor in Chen, OctopusMoving_v3.tex, lines 125–126.

Definition 1.7 (The electrical Dirichlet energy).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.electricEnergy (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

For a real potential h, sum each squared potential difference weighted by its conductance. The factor one half removes the duplication of each undirected edge in the ordered-pair sum. This is the electrical energy in Chen, OctopusMoving_v3.tex, lines 160–165.

Definition 1.8 (The unit-voltage infimum).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.effectiveConductance (✓ std3).

Citation. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

Take the real infimum of electrical energies of potentials equal to one at x and zero at y. For distinct vertices and nonnegative conductances, this set is nonempty and bounded below by zero. It is the reciprocal-effective-resistance expression in Chen, OctopusMoving_v3.tex, line 141. The definition uses the real sInf operation for all arguments, including those for which the unit-voltage conditions are inconsistent.

Definition 1.9 (The converse inequality at every nondegenerate density).

Formalization. D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

Chen, OctopusMoving_v3.tex, lines 177–179, conjectures optimality on finite weighted graphs and on resistance spaces. Here the finite-graph converse says that if a real constant k bounds the exchange cost by k times the exclusion energy for every real observable, then k times the effective conductance is at least one. The quantifiers include every finite vertex type, every nonnegative symmetric conductance, every pair of distinct vertices and every density strictly between zero and one. For the source’s graphs with positive effective conductance, combining this converse with the published upper bound, Theorem 1, lines 131–145, gives the least constant. At zero effective conductance there is no admissible finite real constant. The densities zero and one are excluded: their probability masses are supported on constant configurations, where every swap gradient vanishes.

Theorem 1.10 (Every admissible constant dominates the resistance).

Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.result (✓ std3). ∎

Resolves. Problems/chen-2017-exclusion-moving-particle-optimality (proved) by D5/S3/StatisticalMechanics/ParticleProcesses/ExclusionMovingParticleOptimality.result.

Source. Repository-derived.

Acknowledgement. Joe P. Chen (2017). The moving particle lemma for the exclusion process on a weighted graph. DOI: 10.1214/17-ECP82. URL: https://arxiv.org/abs/1606.01577v4.

Commentary.

For a real potential h, use the linear occupation observable Fₕ: at ζ its value is the sum over z of h(z) times the natural value of ζ(z), cast to ℝ. For distinct u and w, only these two summands change under the swap. Subtracting gives (h(u) − h(w)) times the difference between the real casts of the occupations at w and u.

First compute expectations of products of single-coordinate functions g: the product mass lets the configuration sum factor into the product over z of (1 − α)g(z,0) + αg(z,1). Choosing one coordinate gives expected occupation α; choosing distinct coordinates u and w gives expected product α². Each real occupation has square equal to itself. Expanding the squared occupation difference therefore gives expectation 2α(1 − α).

Expectation sends the zero function to zero and commutes with multiplication by a real constant. For u equal to w the swap gradient and the potential difference both vanish. For distinct u and w, square the gradient formula and pull out the squared potential difference. Thus for all u and w the expected squared gradient of Fₕ is 2α(1 − α)(h(u) − h(w))². Substitution into the ordered-pair sum gives exclusionEnergy(c,α,Fₕ) = α(1 − α) electricEnergy(c,h). If h(x) = 1 and h(y) = 0, half the expected squared x,y-gradient is α(1 − α).

Nonnegative conductances make every electrical energy nonnegative. For distinct x and y the potential equal to one at x and zero elsewhere satisfies the unit-voltage conditions, so the feasible energy set is nonempty. Suppose 1 ≤ k electricEnergy(c,h) for every feasible h. Testing any such potential shows k > 0: otherwise its nonnegative energy would make the right side nonpositive. Division by k shows that 1/k bounds every feasible energy from below. The defining infimum is consequently at least 1/k, and multiplication by k gives 1 ≤ k effectiveConductance(c,x,y).

Finally fix the finite conductance network, distinct x and y, density 0 < α < 1 and an admissible k. For each unit-voltage potential h, apply the assumed moving-particle bound to Fₕ. The two identities give α(1 − α) ≤ k α(1 − α) electricEnergy(c,h). Since α(1 − α) is positive, cancellation yields 1 ≤ k electricEnergy(c,h) for every feasible h. The infimum argument proves the conclusion.

References