Open Research Index

Davis-Kahan 1970: the four Section 2 rotation-of-eigenvectors theorem families

Jon Crall, Edward Wang

Palomar Registrypalomar/PALOMAR-2026-09-17-000001Sep 17, 2026math.FAscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-17-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-17-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-17-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'