WIP: Import Davis–Kahan rotation of eigenvectors

LeanPool/DavisKahan/DavisKahan.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 Kitware, Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, GPT 5.6 High
+-/
+module
+
+public import LeanPool.DavisKahan.DavisKahan.BoundedOperator.All
+public import LeanPool.DavisKahan.DavisKahan.FiniteDimensional.All
+public import LeanPool.DavisKahan.DavisKahan.Sources.All
+
+/-!
+# Davis--Kahan perturbation theory
+
+The deliberate public umbrella: supported bounded-operator and
+finite-dimensional theory together with the production source aggregate.
+Specialized endpoints, alternative proofs, and experiments require explicit
+imports.
+-/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/All.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Kitware, Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, OpenAI GPT-5.6 Thinking
+-/
+module
+
+public import LeanPool.DavisKahan.DavisKahan
+public import LeanPool.DavisKahan.DavisKahan.Alternative.All
+public import LeanPool.DavisKahan.DavisKahan.Analysis.All
+public import LeanPool.DavisKahan.DavisKahan.BoundedOperator.All
+public import LeanPool.DavisKahan.DavisKahan.DoubleAngle.All
+public import LeanPool.DavisKahan.DavisKahan.FiniteDimensional.All
+public import LeanPool.DavisKahan.DavisKahan.Geometry.All
+public import LeanPool.DavisKahan.DavisKahan.InfiniteDimensional.All
+public import LeanPool.DavisKahan.DavisKahan.OperatorIdeal.All
+public import LeanPool.DavisKahan.DavisKahan.Riccati.All
+public import LeanPool.DavisKahan.DavisKahan.SharedFoundations.All
+public import LeanPool.DavisKahan.DavisKahan.SinTheta.All
+public import LeanPool.DavisKahan.DavisKahan.Sources.All
+public import LeanPool.DavisKahan.DavisKahan.Specialized.All
+public import LeanPool.DavisKahan.DavisKahan.SpectralTheory.All
+public import LeanPool.DavisKahan.DavisKahan.Sylvester.All
+public import LeanPool.DavisKahan.DavisKahan.TanTheta.All
+public import LeanPool.DavisKahan.DavisKahan.TanTwoTheta.All
+
+/-! # `DavisKahan` -/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/Alternative.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2026 Jon Crall, Edward Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, Edward Wang
+-/
+module
+
+
+public import LeanPool.DavisKahan.DavisKahan.Alternative.All
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional
+
+/-! Supporting modules for Davis–Kahan rotation of eigenvectors. -/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/Alternative/All.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2026 Kitware, Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, OpenAI GPT-5.6 Thinking
+-/
+module
+
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.All
+
+/-! # `DavisKahan/Alternative` -/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/Alternative/FiniteDimensional.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Jon Crall, Edward Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, Edward Wang
+-/
+module
+
+
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.All
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.EigenbasisFrobenius
+
+/-! Supporting modules for Davis–Kahan rotation of eigenvectors. -/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/Alternative/FiniteDimensional/API.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Jon Crall, Edward Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, Edward Wang
+-/
+module
+
+
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API.All
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API.ClassicalProseLike
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API.ProseLike
+
+/-! Supporting modules for Davis–Kahan rotation of eigenvectors. -/
+
+@[expose] public section

LeanPool/DavisKahan/DavisKahan/Alternative/FiniteDimensional/API/All.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 Kitware, Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Crall, OpenAI GPT-5.6 Thinking
+-/
+module
+
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API.ClassicalProseLike
+public import LeanPool.DavisKahan.DavisKahan.Alternative.FiniteDimensional.API.ProseLike
+
+/-! # `DavisKahan/Alternative/FiniteDimensional/API` -/
+
+@[expose] public section