WIP: Import Davis–Kahan rotation of eigenvectors - #511

Open

Vilin97 wants to merge 89 commits into

mainfrom

codex/import42-aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization

Commits on Sep 21, 2026

Import Davis–Kahan rotation of eigenvectors with source attribution and complete production scope
Vilin97
committed
69ecb75
Port complete upstream content to current Mathlib and improve lint compliance
Vilin97
committed
1ce49ea
Port Lp measurability and spectral operator support
Vilin97
committed
bd8c2ff
Port operator ideal APIs and extract projection and cutoff estimates
Vilin97
committed
f4e288b
Port spectral measure APIs and factor cutoff estimates
Vilin97
committed
f3fe649
Refactor operator estimates and clear tactic compatibility warnings
Vilin97
committed
2d12c7a
Factor spectral mass and beam boundary proofs into supporting lemmas
Vilin97
committed
385edbd
Isolate the quarter-angle scalar comparison
Vilin97
committed
01d3ba0
Factor Gram-band assembly and strict Lyapunov form proofs
Vilin97
committed
c2c9295
Separate Lyapunov spectral and reflection angle estimates
Vilin97
committed
059f5a9
Extract reflection compression and Gram identities
Vilin97
committed
04414c1
Factor angular projection identities and double-angle modulus formula
Vilin97
committed
b8e6ca2
Separate invariant-plane form estimates from the eigenvector tangent bound
Vilin97
committed
54f3e92
Make noncomputable declaration scopes explicit and normalize source style
Vilin97
committed
0068dad
Document Davis–Kahan APIs and normalize declaration names and simp attributes
Vilin97
committed
e00fd09

Commits on Sep 22, 2026

Remove unused class and scalar assumptions from Davis Kahan lemmas
Vilin97
committed
a42b3e7
Remove remaining unused Hilbert space assumptions
Vilin97
committed
4bead46
Trim whitespace after assumption cleanup
Vilin97
committed
23c84f6
Generalize further operator ideal statements by dropping unused classes
Vilin97
committed
689edb2
Separate polar factorization certificates from operator data
Vilin97
committed
c8a84bd
Remove propagated unused operator completeness assumptions
Vilin97
committed
7870208
Trim remaining inherited completeness requirements
Vilin97
committed
f18542e
Remove final propagated redundant operator completeness assumptions
Vilin97
committed
4a97a85
Generalize derived gauge estimates by removing unused completeness
Vilin97
committed
b1468a2
Remove remaining completeness assumptions from contraction bound
Vilin97
committed
05d8740
Clean blank proof lines and compiler-suggested formatting
Vilin97
committed
7c75810
Wrap long Davis Kahan proofs in ten verified modules
Vilin97
committed
56b3f86
Merge remote-tracking branch 'origin/main' into pr-511
github-actions[bot]
committed
09e456d

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Commits on Sep 25, 2026

Commits on Sep 26, 2026

Commits on Sep 27, 2026

Commits on Sep 28, 2026

Commits on Sep 29, 2026

Merge remote-tracking branch 'origin/main' into pr-511
github-actions[bot]
committed
50d0550
Remove no-op expose annotations in Davis-Kahan
Vilin97
committed
937aa7a