Variance and edge curvature

Abstract

A finite variance inequality for reversible birth-and-death rates.

Definition 1.1 (Edge curvature).

$\forall p \in N a t \to R e a l, \forall r \in N a t \to R e a l, \forall i \in N a t, kappa (p, r, i) = p (i) - p (i + 1) + r (i + 1) - r (i)$

Formalization. D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.kappa (✓ std3).

Source. Repository-derived.

Acknowledgement. Dmitrii Karp and Yi Zhang (2023). Log-concavity and log-convexity of series containing multiple Pochhammer symbols. DOI: 10.1007/s13540-023-00238-0. URL: https://arxiv.org/abs/2305.09029.

Commentary.

For all real sequences p and r and every natural i, kappa(p,r,i) equals p(i)-p(i+1)+r(i+1)-r(i).

Definition 1.2 (Finite variance).

$\forall n \in N a t, \forall p i \in N a t \to R e a l, \forall h \in N a t \to R e a l, variance (n, p i, h) = i \in Finset . range (n + 1) \sum (p i (i) \cdot h (i) - j \in Finset . range (n + 1) \sum (p i (j) \cdot h (j))^{2})$

Formalization. D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.variance (✓ std3).

Source. Repository-derived.

Commentary.

For a natural n and real sequences pi and h, set a equal to the sum of pi(j)h(j) over 0 <= j <= n. Then variance(n,pi,h) is the sum over 0 <= i <= n of pi(i) times (h(i)-a) squared. Under probability normalization this is the usual variance.

Theorem 1.3 (Curvature-weighted variance bound).

$\forall n \in N a t, \forall p i \in N a t \to R e a l, \forall p \in N a t \to R e a l, \forall r \in N a t \to R e a l, \forall h \in N a t \to R e a l, (\forall i \in N a t, i \leq n \Rightarrow 0 < p i (i)) \Rightarrow i \in Finset . range (n + 1) \sum (p i (i)) = 1 \Rightarrow p (n) = 0 \Rightarrow r (0) = 0 \Rightarrow (\forall i \in N a t, i < n \Rightarrow 0 < p (i)) \Rightarrow (\forall i \in N a t, 0 < i \Rightarrow (i \leq n \Rightarrow 0 < r (i))) \Rightarrow (\forall i \in N a t, i < n \Rightarrow p i (i) \cdot p (i) = p i (i + 1) \cdot r (i + 1)) \Rightarrow (\forall i \in N a t, i < n \Rightarrow 0 < kappa (p, r, i)) \Rightarrow variance (n, p i, h) \leq i \in Finset . range (n) \sum (\frac{p i ( i ) \cdot p ( i )}{kappa ( p , r , i )} \cdot (h (i + 1) - h (i))^{2})$

Proof. Machine-checked in Lean as D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.variance_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let n be any natural number. Suppose pi is positive on the vertices 0,…,n and sums to one there. Let p(n)=r(0)=0, let p(i)>0 for i<n, and let r(i)>0 for 0<i<=n. Assume detailed balance pi(i)p(i)=pi(i+1)r(i+1) and positive kappa(p,r,i) for every i<n. Then, for every real sequence h, variance(n,pi,h) is at most the sum over 0 <= i < n of pi(i)p(i)/kappa(p,r,i) times (h(i+1)-h(i)) squared. The hypotheses allow n=0, when the variance and the edge sum vanish.

Center h by its pi mean. An edge flux z is obtained by taking the negative cumulative centered mass and dividing by the edge weight. It satisfies h(i)=r(i)z(i)-p(i)z(i+1). Detailed balance converts the variance into the edge sum of pi(i)p(i)(h(i+1)-h(i))z(i+1). A pointwise square inequality and the same balance identity bound the sum of pi(i)p(i)kappa(i)z(i+1) squared by the variance. Weighted Cauchy-Schwarz then gives the stated estimate. All sums are finite, and no inverse operator or limiting argument is needed.

References

Truth anchor: D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.kappa
Truth anchor: D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.variance
Truth anchor: D5/S3/Analytic/KarpZhangReciprocal/BirthDeath.variance_bound

Keyboard shortcuts

trureturing — Discovering truth

Variance and edge curvature

Abstract

References