{"id":"palomar/PALOMAR-2026-09-17-000001","url":"https://github.com/AIQ-Kitware/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization/tree/38e37da6e147cd0016da1eb05987c3edf7d95b39","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-17-000001-v1.json","repo":"https://github.com/AIQ-Kitware/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization","tags":["math.FA","math.NA","msc:47A55","msc:47A15","msc:15A42","msc:65F15","spectral-theory","perturbation-theory","numerical-linear-algebra","lean-formalization"],"score":0,"title":"Davis-Kahan 1970: the four Section 2 rotation-of-eigenvectors theorem families","trust":"high","domain":"math.FA","source":"palomar","authors":["Jon Crall","Edward Wang"],"reviews":0,"subject":"math.FA","summary":"Machine-checked Lean 4 presentation of the four headline theorem families in Section 2 of Davis and Kahan (1970): sin-Theta, tan-Theta, sin-2-Theta, and tan-2-Theta. The Palomar Comparator exposes five selected source-facing declarations: the residual sin-Theta estimate, the residual tan-Theta estimate, both the residual and whole-space sin-2-Theta estimates, and the residual tan-2-Theta estimate. The statements retain the paper's standing separable ambient Hilbert-space scope, permit finite or infinite ambient dimension, and are generic over RCLike scalars to cover the real and complex…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-17","reactions":{},"formalized":true,"formalizes":[{"title":"The rotation of eigenvectors by a perturbation. III","identifier":"doi:10.1137/0707001","relationship":"formalizes"}]}