Entrywise nonnegativity of the matrix Neumann series
ProvedChenWhitt93.Reflection.neumann_series_entry_nonnegchen-whitt-1993entrywise-nonnegativityneumann-seriesreflection-map
An entrywise-nonnegative real matrix with summable powers has an entrywise-nonnegative Neumann series sum.
Preamble
import Mathlib open Filter Topology Matrix
Formal statement
namespace ChenWhitt93.Reflection
/-- An entrywise-nonnegative matrix with summable powers has an entrywise-
nonnegative Neumann series sum (feeds the componentwise bound (2.9) via
`(I - Q)^{-1} = sum Q^k >= 0`). -/
theorem neumann_series_entry_nonneg {n : Nat} (Q : Matrix (Fin n) (Fin n) Real)
(hQ : forall i j, 0 <= Q i j) (hsum : Summable (fun k : Nat => Q ^ k)) :
forall i j, 0 <= (tsum fun k : Nat => Q ^ k) i j := by sorry
end ChenWhitt93.ReflectionSource
Chen and Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993), nonnegativity of (I-Q)^{-1} used in Eq. (2.9), p. 339