An Introduction to Matrix Concentration Inequalities Ch 5: Matrix ChernoffTextbook
Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.
The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.
Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.
Shared definitions: Chapter 3; submit that draft first.