HermitianEigenvaluePerturbation

Abstract

Public declarations of HermitianEigenvaluePerturbation, with complete parameters and the Lean operations.

Theorem 1.1 (finrank_span_image).

Lean statement: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.finrank_span_image

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.finrank_span_image (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The complex span of a selected finite orthonormal subfamily has dimension equal to the number of selected indices. No completeness or finite-dimensional ambient instance is used.

Theorem 1.2 (sum_sq_norm_repr_eq_sq_norm).

Lean statement: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.sum_sq_norm_repr_eq_sq_norm

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.sum_sq_norm_repr_eq_sq_norm (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The sum of squared norms of all orthonormal-basis coordinates equals the squared norm of the vector. No completeness or additional finite-dimensional instance is used.

Theorem 1.3 (re_inner_apply_self_eq_sum_eigenvalues_mul_sq).

Lean statement: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.re_inner_apply_self_eq_sum_eigenvalues_mul_sq

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.re_inner_apply_self_eq_sum_eigenvalues_mul_sq (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

For a symmetric endomorphism of a finite-dimensional complex inner-product space, the real quadratic form is the sum of its eigenvalues times the squared eigenbasis coordinates. The basis index n is identified with the finrank by the explicit equality hn.

Theorem 1.4 (abs_eigenvalue_sub_eigenvalue_le_norm).

$$\forall (n:\mathbb{N}),\forall (d:\mathbb{N}),\forall (T:\mathrm{EuclideanSpace}\mathbb{C}(Find){\to }_L[\mathbb{C}]\mathrm{EuclideanSpace}\mathbb{C}(Find)),\forall (S:\mathrm{EuclideanSpace}\mathbb{C}(Find){\to }_L[\mathbb{C}]\mathrm{EuclideanSpace}\mathbb{C}(Find)),\forall (hT:(\mathrm{val}\left(T\right)).\mathrm{IsSymmetric}),\forall (hS:(\mathrm{val}\left(S\right)).\mathrm{IsSymmetric}),\forall (hn:\mathrm{Module}.\mathrm{finrank}\mathbb{C}(\mathrm{EuclideanSpace}\mathbb{C}(Find))=n),\forall (k:Finn),\left|hT.\mathrm{eigenvalues}hnk-hS.\mathrm{eigenvalues}hnk\right|\le \Vert T-S\Vert$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalue_sub_eigenvalue_le_norm (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.5 (norm_toEuclideanLin_le_of_entry_le).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (\epsilon :\mathbb{R}),(\forall (ij:Finn),\Vert Aij\Vert \le \epsilon )\to (\forall (x:\mathrm{EuclideanSpace}\mathbb{C}(Finn)),\Vert (\mathrm{Matrix}.\mathrm{toEuclideanLin}A)x\Vert \le \mathrm{val}\left(n\right)\cdot \epsilon \cdot \Vert x\Vert )$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.norm_toEuclideanLin_le_of_entry_le (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.6 (abs_eigenvalues0_sub_le_norm).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (B:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\forall (hB:B.\mathrm{IsHermitian}),\forall (k:Fin(\mathrm{Fintype}.\mathrm{card}(Finn))),\left|hA.{\mathrm{eigenvalues}}_{0}k-hB.{\mathrm{eigenvalues}}_{0}k\right|\le \Vert \mathrm{Matrix}.\mathrm{toEuclideanCLM}(A-B)\Vert$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalues0_sub_le_norm (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.7 (abs_eigenvalues0_sub_le_of_entry_le).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (\mathrm{Ahat}:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\forall (\mathrm{hAhat}:\mathrm{Ahat}.\mathrm{IsHermitian}),\forall (\epsilon :\mathbb{R}),(\forall (ij:Finn),\Vert \mathrm{Ahat}ij-Aij\Vert \le \epsilon )\to (\forall (k:Fin(\mathrm{Fintype}.\mathrm{card}(Finn))),\left|\mathrm{hAhat}.{\mathrm{eigenvalues}}_{0}k-hA.{\mathrm{eigenvalues}}_{0}k\right|\le \mathrm{val}\left(n\right)\cdot \epsilon )$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalues0_sub_le_of_entry_le (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.8 (exists_unit_vector_re_inner_le_eigenvalue).

$$\forall E\in \mathrm{Type}\left(\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{InnerProductSpace}\left(\mathrm{Complex},E\right)]\forall n\in \mathrm{Nat},[\mathrm{FiniteDimensional}\left(\mathrm{Complex},E\right)]\forall T\in E{\to }_L[\mathrm{Complex}]E,\forall hT\in \mathrm{LinearMap}.\mathrm{IsSymmetric}\left(T\right),\forall hn\in \mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},E\right)=n,\forall k\in \mathrm{Fin}\left(n\right),\forall V\in \mathrm{Submodule}\left(\mathrm{Complex},E\right),\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},V\right)=\mathrm{Fin}.\mathrm{val}\left(k\right)+1\Rightarrow \left(\exists x\in E,x\in V\wedge \left(\Vert x\Vert =1\wedge \mathrm{RCLike}.\mathrm{re}\left(\mathrm{inner}\left(\mathrm{Complex},T\left(x\right),x\right)\right)\le hT.\mathrm{eigenvalues}\left(hn,k\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.exists_unit_vector_re_inner_le_eigenvalue (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

Every subspace of dimension k plus one contains a unit vector whose real Rayleigh value is at most the k-th ordered eigenvalue.

Theorem 1.9 (exists_submodule_forall_unit_eigenvalue_le_re_inner).

$$\forall E\in \mathrm{Type}\left(\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{InnerProductSpace}\left(\mathrm{Complex},E\right)]\forall n\in \mathrm{Nat},[\mathrm{FiniteDimensional}\left(\mathrm{Complex},E\right)]\forall T\in E{\to }_L[\mathrm{Complex}]E,\forall hT\in \mathrm{LinearMap}.\mathrm{IsSymmetric}\left(T\right),\forall hn\in \mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},E\right)=n,\forall k\in \mathrm{Fin}\left(n\right),\exists V\in \mathrm{Submodule}\left(\mathrm{Complex},E\right),\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},V\right)=\mathrm{Fin}.\mathrm{val}\left(k\right)+1\wedge \left(\forall x\in E,x\in V\Rightarrow \left(\Vert x\Vert =1\Rightarrow hT.\mathrm{eigenvalues}\left(hn,k\right)\le \mathrm{RCLike}.\mathrm{re}\left(\mathrm{inner}\left(\mathrm{Complex},T\left(x\right),x\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.exists_submodule_forall_unit_eigenvalue_le_re_inner (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

There is a subspace of dimension k plus one on which every unit vector has real Rayleigh value at least the k-th ordered eigenvalue.

Theorem 1.10 (abs_eigenvalue_sub_eigenvalue_le).

$$\forall E\in \mathrm{Type}\left(\right),[\mathrm{NormedAddCommGroup}\left(E\right)][\mathrm{InnerProductSpace}\left(\mathrm{Complex},E\right)]\forall n\in \mathrm{Nat},[\mathrm{FiniteDimensional}\left(\mathrm{Complex},E\right)]\forall T\in E{\to }_L[\mathrm{Complex}]E,\forall S\in E{\to }_L[\mathrm{Complex}]E,\forall hT\in \mathrm{LinearMap}.\mathrm{IsSymmetric}\left(T\right),\forall hS\in \mathrm{LinearMap}.\mathrm{IsSymmetric}\left(S\right),\forall hn\in \mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},E\right)=n,\forall epsilon\in \mathrm{Real},\left(\forall x\in E,\Vert (T-S)\left(x\right)\Vert \le epsilon\cdot \Vert x\Vert \right)\Rightarrow \left(\forall k\in \mathrm{Fin}\left(n\right),\left|hT.\mathrm{eigenvalues}\left(hn,k\right)-hS.\mathrm{eigenvalues}\left(hn,k\right)\right|\le epsilon\right)$$

Proof. Machine-checked in Lean as D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalue_sub_eigenvalue_le (✓ std3). ∎

Citation. Jon Crall and LeanPool contributors (2026). LeanPool DavisKahan Hermitian eigenvalue perturbation proofs. URL: https://github.com/LeanPool/lean-pool/blob/bbc67ff1e3ac4fc6a969daf42985a0d8f988d0b8.

Commentary.

A pointwise norm bound on the difference of symmetric linear maps bounds the difference of corresponding ordered eigenvalues.

References

• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalue_sub_eigenvalue_le
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalue_sub_eigenvalue_le_norm
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalues0_sub_le_norm
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.abs_eigenvalues0_sub_le_of_entry_le
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.exists_submodule_forall_unit_eigenvalue_le_re_inner
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.exists_unit_vector_re_inner_le_eigenvalue
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.finrank_span_image
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.norm_toEuclideanLin_le_of_entry_le
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.re_inner_apply_self_eq_sum_eigenvalues_mul_sq
• Truth anchor: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation.sum_sq_norm_repr_eq_sq_norm