{"id":"palomar/PALOMAR-2026-09-18-000005","url":"https://github.com/AIQ-Kitware/aiq-yu-wang-samworth-2015-useful-variant-davis-kahan-statisticians-formalization/tree/234e61473e5378fd89585d8929cfba560b046323","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-18-000005-v1.json","repo":"https://github.com/AIQ-Kitware/aiq-yu-wang-samworth-2015-useful-variant-davis-kahan-statisticians-formalization","tags":["math.ST","math.FA","msc:62H25","msc:47A55","msc:15A42","msc:15A18","msc:65F15","statistics","matrix-perturbation","lean"],"score":0,"title":"Yu-Wang-Samworth 2015: population-gap eigenspace and singular-subspace perturbation bounds","trust":"high","domain":"math.ST","source":"palomar","authors":["Jon Crall","Edward Wang"],"reviews":0,"subject":"math.ST","summary":"A machine-checked Lean 4 formalization of the principal population-gap perturbation results of Yi Yu, Tengyao Wang and Richard J. Samworth, \"A useful variant of the Davis-Kahan theorem for statisticians\" (Biometrika 102 (2015) 315-323). This single Palomar entry compares both conclusions of Theorem 2 and both displays of Corollary 1 for eigenspaces of real symmetric matrices, together with the right- and left-singular-subspace conclusions of Theorem 3 for general real matrices and two supporting equivalences between its Gram-eigenvector formulation and the paper's paired singular-vector…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-18","reactions":{},"formalized":true,"formalizes":[{"title":"A useful variant of the Davis-Kahan theorem for statisticians","identifier":"doi:10.1093/biomet/asv008","relationship":"adapts"}]}