Neumann inverse identity for a summable matrix geometric series
ProvedChenWhitt93.Reflection.neumann_inverse_identitychen-whitt-93decompositionneumann-seriesqueueingreflection-map
If the matrix power series sum_{k} Q^k is summable, its sum is a two-sided inverse of (I - Q).
Preamble
import Mathlib open Filter Topology Matrix
Formal statement
namespace ChenWhitt93.Reflection
/-- If the matrix geometric series `sum k, Q ^ k` is summable, its tsum is a
two-sided inverse of `1 - Q` (used in Eq. (2.10) for `(I - Q)^{-1} = sum Q^k`). -/
theorem neumann_inverse_identity {n : Nat} (Q : Matrix (Fin n) (Fin n) Real)
(hsum : Summable (fun k : Nat => Q ^ k)) :
(tsum fun k : Nat => Q ^ k) * (1 - Q) = 1 /\
(1 - Q) * (tsum fun k : Nat => Q ^ k) = 1 := by sorry
end ChenWhitt93.ReflectionSource
Chen and Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993), Eq. (2.10) Neumann expansion of (I-Q)^{-1}, p. 339