Bessel's inequality for a… to The interval/exterior Sylvester…

TheoremBessel's inequality for a functional#

The values of a continuous linear functional φ on an orthonormal family are square summable. The space need not be complete.

Orthonormal.summable_norm_apply_sq.{u_1, u_2, u_3} {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : ι → E} (hv : Orthonormal 𝕜 v)
  (φ : StrongDual 𝕜 E) : Summable fun i => ‖φ (v i)‖ ^ 2
Lean

Formalized in Tau Ceti as Orthonormal.summable_norm_apply_sq.

Other forms

Bessel's inequality for the left singular vectors. Formalized in Tau Ceti as LinearMap.sum_norm_inner_leftSingularVector_sq_le.

LinearMap.sum_norm_inner_leftSingularVector_sq_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
  [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : F) :
  ∑ i, ‖inner 𝕜 (A.leftSingularVector i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality for the analysis map of an orthonormal family. Formalized in Tau Ceti as Orthonormal.norm_analysisMap_le.

Orthonormal.norm_analysisMap_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E}
  (hv : Orthonormal 𝕜 v) (x : E) : ‖(TauCeti.analysisMap 𝕜 v) x‖ ≤ ‖x‖
Sources
LeanOrthonormal.summable_norm_apply_sq · LinearMap.sum_norm_inner_leftSingularVector_sq_le · Orthonormal.norm_analysisMap_le
Used by 1
Used byKy Fan's maximum principle, attainment

TheoremCauchy–Schwarz for the column series#

∑' i, ‖⟪bᵢ, x⟫‖ ‖fᵢ‖ ≤ ‖x‖ ‖f‖.

HilbertBasis.tsum_norm_inner_mul_norm_le.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [NormedAddCommGroup F] (b : HilbertBasis ι 𝕜 E) (f : ↥(lp (fun x => F) 2)) (x : E) :
  ∑' (i : ι), ‖inner 𝕜 (b i) x‖ * ‖↑f i‖ ≤ ‖x‖ * ‖f‖
Lean

Formalized in Tau Ceti as HilbertBasis.tsum_norm_inner_mul_norm_le.

Other forms

Cauchy–Schwarz for the defect form of an operator. Formalized in Tau Ceti as ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le.

ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (X : F →L[𝕜] E) (v w : F) :
  (‖X‖ ^ 2 * RCLike.re (inner 𝕜 v w) - RCLike.re (inner 𝕜 (X v) (X w))) ^ 2 ≤
    (‖X‖ ^ 2 * ‖v‖ ^ 2 - ‖X v‖ ^ 2) * (‖X‖ ^ 2 * ‖w‖ ^ 2 - ‖X w‖ ^ 2)
Sources
LeanHilbertBasis.tsum_norm_inner_mul_norm_le · ContinuousLinearMap.sq_opNorm_sq_mul_re_inner_sub_re_inner_le
Used by 3
Used byHilbert–Schmidt norm identity · The reverse separated Sylvester bound · The separated Sylvester bound

TheoremThe Cotlar–Stein lemma#

Let T i be operators between Hilbert spaces which are almost orthogonal in the sense that ∑ j, √‖(T i)† ∘L T j‖ ≤ A and ∑ j, √‖T i ∘L (T j)†‖ ≤ A for every i, the sums over j being taken over arbitrary finite sets. Then for every x the series ∑ i, T i x converges unconditionally, and its sum is a bounded operator of norm at most A.

TauCeti.exists_hasSum_apply_of_almost_orthogonal.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F]
  (T : ι → E →L[𝕜] F) {A : ℝ} (hA : 0 ≤ A)
  (h₁ : ∀ (i : ι) (s : Finset ι), ∑ j ∈ s, √‖ContinuousLinearMap.adjoint (T i) ∘SL T j‖ ≤ A)
  (h₂ : ∀ (i : ι) (s : Finset ι), ∑ j ∈ s, √‖T i ∘SL ContinuousLinearMap.adjoint (T j)‖ ≤ A) :
  ∃ S, ‖S‖ ≤ A ∧ ∀ (x : E), HasSum (fun i => (T i) x) (S x)
Lean

Formalized in Tau Ceti as TauCeti.exists_hasSum_apply_of_almost_orthogonal.

Other forms

The Cotlar–Stein lemma, finite form. Formalized in Tau Ceti as TauCeti.norm_sum_le_of_almost_orthogonal.

TauCeti.norm_sum_le_of_almost_orthogonal.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F]
  (T : ι → E →L[𝕜] F) {A : ℝ} (s : Finset ι) (hA : 0 ≤ A)
  (h₁ : ∀ i ∈ s, ∑ j ∈ s, √‖ContinuousLinearMap.adjoint (T i) ∘SL T j‖ ≤ A)
  (h₂ : ∀ i ∈ s, ∑ j ∈ s, √‖T i ∘SL ContinuousLinearMap.adjoint (T j)‖ ≤ A) : ‖∑ i ∈ s, T i‖ ≤ A
Sources
LeanTauCeti.exists_hasSum_apply_of_almost_orthogonal · TauCeti.norm_sum_le_of_almost_orthogonal

TheoremCourant–Fischer, lower direction#

There is a subspace V of dimension k + 1 on which every unit vector x satisfies λₖ(T) ≤ re ⟪T x, x⟫, where λ is the decreasing enumeration LinearMap.IsSymmetric.eigenvalues of the eigenvalues of the symmetric operator T.

Witness: V = span {bᵢ : i ≤ k}; on it the quadratic form is bounded below by λₖ since all involved eigenvalues are ≥ λₖ.

LinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ}
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (k : Fin n) :
  ∃ V,
    Module.finrank 𝕜 ↥V = ↑k + 1 ∧
      ∀ x ∈ V, ‖x‖ = 1 → hT.eigenvalues hn k ≤ RCLike.re (inner 𝕜 (T x) x)
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner.

Other forms

Courant–Fischer, upper direction. Formalized in Tau Ceti as LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue.

LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ}
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (k : Fin n) (V : Submodule 𝕜 E) (hV : Module.finrank 𝕜 ↥V = ↑k + 1) :
  ∃ x ∈ V, ‖x‖ = 1 ∧ RCLike.re (inner 𝕜 (T x) x) ≤ hT.eigenvalues hn k

Courant–Fischer, upper direction, for large subspaces. Formalized in Tau Ceti as LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue_of_le_finrank.

LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue_of_le_finrank.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ}
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (k : Fin n) (V : Submodule 𝕜 E) (hV : ↑k + 1 ≤ Module.finrank 𝕜 ↥V) :
  ∃ x ∈ V, ‖x‖ = 1 ∧ RCLike.re (inner 𝕜 (T x) x) ≤ hT.eigenvalues hn k
Sources
LeanLinearMap.IsSymmetric.exists_submodule_forall_unit_eigenvalue_le_re_inner · LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue · LinearMap.IsSymmetric.exists_unit_vector_re_inner_le_eigenvalue_of_le_finrank
Used by 11
Used byFan dominance · The pairwise Sylvester bound · The perturbation Davis–Kahan sin Θ theorem · The residual Davis–Kahan sin Θ theorem · The Davis–Kahan sin 2Θ theorem · The interval/exterior Sylvester bound · The pairwise π / 2 Davis–Kahan sin Θ theorem · Sylvester bound from a disc and the exterior of a larger disc · The singular-value Hoffman–Wielandt inequality · Weyl's inequality · Eckart–Young for Ky Fan gauges

TheoremDavis's eigenvalue-change lower bound#

Let T and S be symmetric, let (vᵢ) be the eigenbasis of T, and suppose the eigenvalues μᵢ of S are pairwise at distance at least γ ≥ 0. If the diagonal entries hᵢ = Re⟪vᵢ, (S - T) vᵢ⟫ of the perturbation satisfy ∑ᵢ hᵢ² ≤ (γ / √2)², then the sorted spectra satisfy

∑ᵢ hᵢ² - (∑ᵢ μᵢ² - ∑ᵢ Re⟪vᵢ, S vᵢ⟫²) ≤ ∑ᵢ (μᵢ - λᵢ)²,

where λᵢ are the eigenvalues of T. Here ∑ᵢ μᵢ² - ∑ᵢ Re⟪vᵢ, S vᵢ⟫² is the squared Frobenius norm of the off-diagonal part of S - T in the basis (vᵢ).

LinearMap.IsSymmetric.le_sum_sq_eigenvalues_sub.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ}
  (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {γ : ℝ} (hγ : 0 ≤ γ)
  (hsep : Pairwise fun i j => γ ≤ |hS.eigenvalues hn i - hS.eigenvalues hn j|)
  (hH :
    ∑ i,
        RCLike.re (inner 𝕜 ((hT.eigenvectorBasis hn) i) ((S - T) ((hT.eigenvectorBasis hn) i))) ^
          2 ≤
      (γ / √2) ^ 2) :
  ∑ i, RCLike.re (inner 𝕜 ((hT.eigenvectorBasis hn) i) ((S - T) ((hT.eigenvectorBasis hn) i))) ^ 2 -
      (∑ i, hS.eigenvalues hn i ^ 2 -
        ∑ i,
          RCLike.re (inner 𝕜 ((hT.eigenvectorBasis hn) i) (S ((hT.eigenvectorBasis hn) i))) ^ 2) ≤
    ∑ i, (hS.eigenvalues hn i - hT.eigenvalues hn i) ^ 2
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.le_sum_sq_eigenvalues_sub.

Sources
LeanLinearMap.IsSymmetric.le_sum_sq_eigenvalues_sub

TheoremDavis's sin 2θ theorem, angle form#

Under the hypotheses of sin_two_theta_le, with θ = arccos ‖P x‖ the angle between the unit eigenvector x and the invariant subspace U,

(b - a) * sin (2θ) ≤ 2 * ε, with no division by b-a.

LinearMap.IsSymmetric.sin_two_arccos_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric)
  (hH : H.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hUinv : ∀ u ∈ U, T u ∈ U)
  {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u))
  (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖)
  {x : E} (hx : ‖x‖ = 1) {μ : ℝ} (hμ : T x + H x = ↑μ • x) :
  (b - a) * Real.sin (2 * Real.arccos ‖U.starProjection x‖) ≤ 2 * ε
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.sin_two_arccos_le.

Other forms

Davis's sin 2θ theorem, orthogonal-decomposition form. Formalized in Tau Ceti as LinearMap.IsSymmetric.sin_two_theta_le_of_mem.

LinearMap.IsSymmetric.sin_two_theta_le_of_mem.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric)
  (hH : H.IsSymmetric) {U : Submodule 𝕜 E} (hUinv : ∀ u ∈ U, T u ∈ U) {a b ε : ℝ}
  (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u))
  (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖)
  {y z : E} (hyU : y ∈ U) (hzU : z ∈ Uᗮ) (hx : ‖y + z‖ = 1) {μ : ℝ}
  (hμ : T (y + z) + H (y + z) = ↑μ • (y + z)) : (b - a) * (‖y‖ * ‖z‖) ≤ ε

Davis's sin 2θ theorem, per-eigenvector product form. Formalized in Tau Ceti as LinearMap.IsSymmetric.sin_two_theta_le.

LinearMap.IsSymmetric.sin_two_theta_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T H : E →ₗ[𝕜] E} (hT : T.IsSymmetric)
  (hH : H.IsSymmetric) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hUinv : ∀ u ∈ U, T u ∈ U)
  {a b ε : ℝ} (hb : ∀ u ∈ U, b * ‖u‖ ^ 2 ≤ RCLike.re (inner 𝕜 (T u) u))
  (ha : ∀ w ∈ Uᗮ, RCLike.re (inner 𝕜 (T w) w) ≤ a * ‖w‖ ^ 2) (hε : ∀ (v : E), ‖H v‖ ≤ ε * ‖v‖)
  {x : E} (hx : ‖x‖ = 1) {μ : ℝ} (hμ : T x + H x = ↑μ • x) :
  (b - a) * (‖U.starProjection x‖ * ‖x - U.starProjection x‖) ≤ ε
Sources
LeanLinearMap.IsSymmetric.sin_two_arccos_le · LinearMap.IsSymmetric.sin_two_theta_le_of_mem · LinearMap.IsSymmetric.sin_two_theta_le

TheoremThe Davis–Kahan sin 2Θ theorem#

Let A and B be symmetric operators on a finite-dimensional inner product space, let U be invariant under A and V invariant under B. If re ⟪A z, z⟫ ≤ a ‖z‖² on Uᗮ and b ‖y‖² ≤ re ⟪A y, y⟫ on U, then the double-angle operator 2 P_{Uᗮ} P_V P_U satisfies (b - a) N(2 P_{Uᗮ} P_V P_U) ≤ 2 N(B - A) for every unitarily invariant seminorm N. No spectral hypothesis is placed on B.

TauCeti.UnitarilyInvariantSeminorm.mul_map_sinTwoAngleOperator_le_two_mul_map_sub.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 E E) {A B : E →L[𝕜] E}
  (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) {U V : Submodule 𝕜 E} (hU : ∀ x ∈ U, A x ∈ U)
  (hV : ∀ x ∈ V, B x ∈ V) {a b : ℝ} (ha : ∀ z ∈ Uᗮ, RCLike.re (inner 𝕜 (A z) z) ≤ a * ‖z‖ ^ 2)
  (hb : ∀ y ∈ U, b * ‖y‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A y) y)) :
  (b - a) * N ↑(U.sinTwoAngleOperator V) ≤ 2 * N (↑B - ↑A)
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_sinTwoAngleOperator_le_two_mul_map_sub.

Sources
LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_sinTwoAngleOperator_le_two_mul_map_sub
Uses 3
Proof usesCourant–Fischer, lower direction · Fan dominance · The interval/exterior Sylvester bound

TheoremThe dimension-free Davis–Kahan sin Θ theorem for the gap#

Let U be invariant under the symmetric operator A and V invariant under the symmetric operator B. Suppose that the quadratic form of A on U is at least c + g while that of B on Vᗮ is at most c, and that the quadratic form of B on V is at least c' + g while that of A on Uᗮ is at most c'. Then the gap between U and V satisfies g ‖P_U - P_V‖ ≤ ‖B - A‖.

Submodule.mul_projectionGap_le_norm_sub.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E)
  [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hA : (↑A).IsSymmetric)
  (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c c' g : ℝ}
  (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x))
  (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2)
  (hBV' : ∀ x ∈ V, (c' + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (B x) x))
  (hAU' : ∀ x ∈ Uᗮ, RCLike.re (inner 𝕜 (A x) x) ≤ c' * ‖x‖ ^ 2) : g * U.projectionGap V ≤ ‖B - A‖
Lean

Formalized in Tau Ceti as Submodule.mul_projectionGap_le_norm_sub.

Sources
LeanSubmodule.mul_projectionGap_le_norm_sub
Uses 1
Proof usesThe directed Davis–Kahan sin Θ theorem for the directed gap

TheoremThe dimension-free directed Davis–Kahan sin Θ theorem#

Let U be invariant under A and W invariant under the symmetric operator B. If the quadratic form of A on U is at least c + g and that of B on W is at most c, then g ‖P_W P_U‖ ≤ ‖B - A‖. For g > 0 this bounds ‖P_W P_U‖ by ‖B - A‖ / g. Neither completeness nor finite dimension is assumed.

Submodule.mul_norm_starProjection_comp_starProjection_le_norm_sub.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E}
  (U W : Submodule 𝕜 E) [U.HasOrthogonalProjection] [W.HasOrthogonalProjection]
  (hB : (↑B).IsSymmetric) (hU : ∀ x ∈ U, A x ∈ U) (hW : ∀ x ∈ W, B x ∈ W) {c g : ℝ}
  (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x))
  (hBW : ∀ x ∈ W, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :
  g * ‖W.starProjection ∘SL U.starProjection‖ ≤ ‖B - A‖
Lean

Formalized in Tau Ceti as Submodule.mul_norm_starProjection_comp_starProjection_le_norm_sub.

Sources
LeanSubmodule.mul_norm_starProjection_comp_starProjection_le_norm_sub
Uses 1 · Used by 1
Proof usesThe reverse separated Sylvester bound
Used byThe directed Davis–Kahan sin Θ theorem for the directed gap

TheoremThe directed Davis–Kahan sin Θ theorem for the directed gap#

Let U be invariant under A and V invariant under the symmetric operator B. If the quadratic form of A on U is at least c + g and that of B on Vᗮ is at most c, then the directed gap ‖P_{Vᗮ} P_U‖ from U to V satisfies g ‖P_{Vᗮ} P_U‖ ≤ ‖B - A‖.

Submodule.mul_directedProjectionGap_le_norm_sub.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →L[𝕜] E} (U V : Submodule 𝕜 E)
  [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] (hB : (↑B).IsSymmetric)
  (hU : ∀ x ∈ U, A x ∈ U) (hV : ∀ x ∈ V, B x ∈ V) {c g : ℝ}
  (hAU : ∀ x ∈ U, (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x))
  (hBV : ∀ x ∈ Vᗮ, RCLike.re (inner 𝕜 (B x) x) ≤ c * ‖x‖ ^ 2) :
  g * U.directedProjectionGap V ≤ ‖B - A‖
Lean

Formalized in Tau Ceti as Submodule.mul_directedProjectionGap_le_norm_sub.

Sources
LeanSubmodule.mul_directedProjectionGap_le_norm_sub
Uses 1 · Used by 1
Proof usesThe dimension-free directed Davis–Kahan sin Θ theorem
Used byThe dimension-free Davis–Kahan sin Θ theorem for the gap

TheoremForward Schur–Horn inequality, Karamata form#

If φ is convex on a set s containing the eigenvalues of a symmetric operator T, then for every orthonormal basis e, the sum of φ over the diagonal entries Re⟪T (e k), e k⟫ is at most the sum of φ over the eigenvalues.

LinearMap.IsSymmetric.sum_map_re_inner_apply_self_le_sum_map_eigenvalues.{u_1, u_2, u_4}
  {𝕜 : Type u_1} {E : Type u_2} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [Fintype κ] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ}
  (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis κ 𝕜 E) {s : Set ℝ}
  {φ : ℝ → ℝ} (hφ : ConvexOn ℝ s φ) (hs : ∀ (i : Fin n), hT.eigenvalues hn i ∈ s) :
  ∑ k, φ (RCLike.re (inner 𝕜 (T (e k)) (e k))) ≤ ∑ i, φ (hT.eigenvalues hn i)
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.sum_map_re_inner_apply_self_le_sum_map_eigenvalues.

Sources
LeanLinearMap.IsSymmetric.sum_map_re_inner_apply_self_le_sum_map_eigenvalues

TheoremFrobenius identity for the overlap operator#

the squared singular values of the overlap operator sum to the squared Frobenius norm ∑ⱼ ∑ᵢ ‖⟪uᵢ, vⱼ⟫‖² of its matrix.

TauCeti.sum_sq_singularValues_overlapOperator.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {ι : Type u_3} {κ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [Fintype ι] [Fintype κ] (u : ι → E) (v : κ → E) :
  ((TauCeti.overlapOperator 𝕜 u v).singularValues.sum fun x s => s ^ 2) =
    ∑ j, ∑ i, ‖inner 𝕜 (u i) (v j)‖ ^ 2
Lean

Formalized in Tau Ceti as TauCeti.sum_sq_singularValues_overlapOperator.

Sources
LeanTauCeti.sum_sq_singularValues_overlapOperator

TheoremThe Frobenius Sylvester bound#

In finite dimension, if A and B are symmetric and every eigenvalue of A is at distance at least δ from every eigenvalue of B, then δ ‖X‖_F ≤ ‖A X - X B‖_F for every X. In particular every solution of the Sylvester equation A X - X B = C satisfies δ ‖X‖_F ≤ ‖C‖_F.

ContinuousLinearMap.mul_frobenius_le_frobenius_sylvester_apply.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F]
  {A : E →L[𝕜] E} {B : F →L[𝕜] F} {δ : ℝ} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  (h : Module.End.PointSpectraSeparated ↑A ⊤ ↑B ⊤ δ) (X : F →L[𝕜] E) :
  δ * (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 F E) ↑X ≤
    (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 F E) ↑((A.sylvester B) X)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.mul_frobenius_le_frobenius_sylvester_apply.

Sources
LeanContinuousLinearMap.mul_frobenius_le_frobenius_sylvester_apply

TheoremThe Frobenius upper residual bound#

The residuals Rⱼ = λⱼ(T) uⱼ - T uⱼ of the eigenvectors uⱼ of S satisfy ∑_{j ∈ s} ‖Rⱼ‖² ≤ 4 ‖S - T‖_F² for every index block s.

LinearMap.IsSymmetric.sum_norm_smul_sub_apply_eigenvectorBasis_sq_le_four_mul_frobenius_sq.{u_1,
    u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) (s : Finset (Fin n)) :
  ∑ j ∈ s,
      ‖↑(hT.eigenvalues hn j) • (hS.eigenvectorBasis hn) j - T ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤
    4 * (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E E) (S - T) ^ 2
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.sum_norm_smul_sub_apply_eigenvectorBasis_sq_le_four_mul_frobenius_sq.

Sources
LeanLinearMap.IsSymmetric.sum_norm_smul_sub_apply_eigenvectorBasis_sq_le_four_mul_frobenius_sq
Uses 1 · Used by 1
Proof usesThe Hoffman–Wielandt inequality
Used byThe Yu–Wang–Samworth overlap bound, Frobenius form

TheoremHadamard's inequality#

The determinant of a family v in the coordinates of an orthonormal basis has norm at most the product of the norms of the vectors. The family may be linearly dependent.

OrthonormalBasis.norm_det_le_prod_norm.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι]
  (b : OrthonormalBasis ι 𝕜 E) (v : ι → E) : ‖b.toBasis.det v‖ ≤ ∏ i, ‖v i‖
Lean

Formalized in Tau Ceti as OrthonormalBasis.norm_det_le_prod_norm.

Other forms

Hadamard's inequality for wedges. Formalized in Tau Ceti as exteriorPower.norm_ιMulti_le_prod_norm.

exteriorPower.norm_ιMulti_le_prod_norm.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (v : Fin n → E) :
  ‖(exteriorPower.ιMulti ℝ n) v‖ ≤ ∏ i, ‖v i‖

Hadamard's inequality for Gram determinants. Formalized in Tau Ceti as Matrix.det_gram_le_prod_norm_sq.

Matrix.det_gram_le_prod_norm_sq.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι]
  (v : ι → E) : (Matrix.gram 𝕜 v).det ≤ ∏ i, ↑‖v i‖ ^ 2

Hadamard's inequality for Gram determinants, for the real part. Formalized in Tau Ceti as Matrix.re_det_gram_le_prod_norm_sq.

Matrix.re_det_gram_le_prod_norm_sq.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι]
  (v : ι → E) : RCLike.re (Matrix.gram 𝕜 v).det ≤ ∏ i, ‖v i‖ ^ 2

Hadamard's inequality, uniform form. Formalized in Tau Ceti as Matrix.re_det_gram_le_pow.

Matrix.re_det_gram_le_pow.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {v : ι → E} {D : ℝ}
  (hD : ∀ (i : ι), ‖v i‖ ^ 2 ≤ D) : RCLike.re (Matrix.gram 𝕜 v).det ≤ D ^ Fintype.card ι
Sources
LeanOrthonormalBasis.norm_det_le_prod_norm · exteriorPower.norm_ιMulti_le_prod_norm · Matrix.det_gram_le_prod_norm_sq · Matrix.re_det_gram_le_prod_norm_sq · Matrix.re_det_gram_le_pow

TheoremHilbert–Schmidt norm identity#

The Hilbert–Schmidt norm of T_f is the ℓ² norm of f.

HilbertBasis.hilbertSchmidtNorm_columnOperator.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (b : HilbertBasis ι 𝕜 E)
  [CompleteSpace E] (f : ↥(lp (fun x => F) 2)) : (b.columnOperator f).hilbertSchmidtNorm = ‖f‖
Lean

Formalized in Tau Ceti as HilbertBasis.hilbertSchmidtNorm_columnOperator.

Sources
LeanHilbertBasis.hilbertSchmidtNorm_columnOperator
Uses 2
Proof usesCauchy–Schwarz for the column series · Parseval's identity for a functional

TheoremThe Hoffman–Wielandt inequality#

For symmetric T and S with eigenvalues listed in decreasing order and every orthonormal basis e, the squared Euclidean distance between the two spectra is at most the squared Frobenius distance ∑ₖ ‖T eₖ - S eₖ‖² between the operators.

LinearMap.IsSymmetric.sum_sq_eigenvalues_sub_le_sum_sq_norm_apply.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {ι : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] [Fintype ι] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric)
  (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (e : OrthonormalBasis ι 𝕜 E) :
  ∑ i, (hT.eigenvalues hn i - hS.eigenvalues hn i) ^ 2 ≤ ∑ k, ‖T (e k) - S (e k)‖ ^ 2
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.sum_sq_eigenvalues_sub_le_sum_sq_norm_apply.

Sources
LeanLinearMap.IsSymmetric.sum_sq_eigenvalues_sub_le_sum_sq_norm_apply
Used by 3
Used byThe Frobenius upper residual bound · Population-gap sine theorem for arbitrary ordered eigenframes · The Hoffman–Wielandt inequality for Hermitian matrices

TheoremHopf's boundary-point lemma#

Let B = ball y R be a ball in a finite-dimensional real inner product space, let e be a unit vector, and let x₀ = y + R • e be the point where the outward ray in direction e meets the sphere ∂B. If u is continuous on closedBall y R, twice continuously differentiable on B, and differentiable at x₀, is subharmonic on B (0 ≤ Δ u), stays strictly below the value u x₀ inside B and weakly below it on the sphere ∂B, then u leaves x₀ in the direction e at a strictly positive rate: 0 < fderiv ℝ u x₀ e.

The strict inequality is needed only inside the ball, so the theorem applies directly when the boundary sphere has merely a weak bound. The classical form, with a strict maximum over the whole closed ball, is TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall.

TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_ball_of_le_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ}
  {e : E} (hR : 0 < R) (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hlap : ∀ x ∈ Metric.ball y R, 0 ≤ Laplacian.laplacian u x)
  (hlt : ∀ x ∈ Metric.ball y R, u x < u (y + R • e))
  (hle : ∀ x ∈ Metric.sphere y R, u x ≤ u (y + R • e)) : 0 < (fderiv ℝ u (y + R • e)) e
Lean

Formalized in Tau Ceti as TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_ball_of_le_sphere.

Other forms

Hopf's boundary-point lemma for -Δ - b·∇ + c. Formalized in Tau Ceti as TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere.

TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u c : E → ℝ} {b : E → E}
  {y e : E} {R β γ : ℝ} (hR : 0 < R) (he : ‖e‖ = 1)
  (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e)) (hc : ∀ x ∈ Metric.ball y R, 0 ≤ c x)
  (hcγ : ∀ x ∈ Metric.ball y R, c x ≤ γ) (hb : ∀ x ∈ Metric.ball y R, ‖b x‖ ≤ β)
  (hsub : ∀ x ∈ Metric.ball y R, c x * u x ≤ Laplacian.laplacian u x + (fderiv ℝ u x) (b x))
  (hnonneg : 0 ≤ u (y + R • e)) (hlt : ∀ x ∈ Metric.ball y R, u x < u (y + R • e))
  (hle : ∀ x ∈ Metric.sphere y R, u x ≤ u (y + R • e)) : 0 < (fderiv ℝ u (y + R • e)) e

Hopf's boundary-point lemma for -Δ - b·∇ + c, minimum form. Formalized in Tau Ceti as TauCeti.fderiv_neg_of_laplacian_add_fderiv_le_mul_of_gt_ball_of_ge_sphere.

TauCeti.fderiv_neg_of_laplacian_add_fderiv_le_mul_of_gt_ball_of_ge_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u c : E → ℝ} {b : E → E}
  {y e : E} {R β γ : ℝ} (hR : 0 < R) (he : ‖e‖ = 1)
  (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e)) (hc : ∀ x ∈ Metric.ball y R, 0 ≤ c x)
  (hcγ : ∀ x ∈ Metric.ball y R, c x ≤ γ) (hb : ∀ x ∈ Metric.ball y R, ‖b x‖ ≤ β)
  (hsuper : ∀ x ∈ Metric.ball y R, Laplacian.laplacian u x + (fderiv ℝ u x) (b x) ≤ c x * u x)
  (hnonpos : u (y + R • e) ≤ 0) (hgt : ∀ x ∈ Metric.ball y R, u (y + R • e) < u x)
  (hge : ∀ x ∈ Metric.sphere y R, u (y + R • e) ≤ u x) : (fderiv ℝ u (y + R • e)) e < 0

Hopf's boundary-point lemma for harmonic functions. Formalized in Tau Ceti as TauCeti.fderiv_pos_of_harmonicOnNhd_of_lt_closedBall.

TauCeti.fderiv_pos_of_harmonicOnNhd_of_lt_closedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ} {e : E} (hR : 0 < R)
  (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball y R))
  (hmax : ∀ x ∈ Metric.closedBall y R, x ≠ y + R • e → u x < u (y + R • e)) :
  0 < (fderiv ℝ u (y + R • e)) e

Hopf's boundary-point lemma for harmonic functions, minimum form. Formalized in Tau Ceti as TauCeti.fderiv_neg_of_harmonicOnNhd_of_gt_closedBall.

TauCeti.fderiv_neg_of_harmonicOnNhd_of_gt_closedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ} {e : E} (hR : 0 < R)
  (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hharm : InnerProductSpace.HarmonicOnNhd u (Metric.ball y R))
  (hmin : ∀ x ∈ Metric.closedBall y R, x ≠ y + R • e → u (y + R • e) < u x) :
  (fderiv ℝ u (y + R • e)) e < 0

Hopf's boundary-point lemma, classical form. Formalized in Tau Ceti as TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall.

TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ} {e : E} (hR : 0 < R)
  (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hlap : ∀ x ∈ Metric.ball y R, 0 ≤ Laplacian.laplacian u x)
  (hmax : ∀ x ∈ Metric.closedBall y R, x ≠ y + R • e → u x < u (y + R • e)) :
  0 < (fderiv ℝ u (y + R • e)) e

Hopf's boundary-point lemma, minimum form. Formalized in Tau Ceti as TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_ball_of_ge_sphere.

TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_ball_of_ge_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ}
  {e : E} (hR : 0 < R) (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hlap : ∀ x ∈ Metric.ball y R, Laplacian.laplacian u x ≤ 0)
  (hgt : ∀ x ∈ Metric.ball y R, u (y + R • e) < u x)
  (hge : ∀ x ∈ Metric.sphere y R, u (y + R • e) ≤ u x) : (fderiv ℝ u (y + R • e)) e < 0

Hopf's boundary-point lemma, minimum form. Formalized in Tau Ceti as TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_closedBall.

TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_closedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {y : E} {R : ℝ} {e : E} (hR : 0 < R)
  (he : ‖e‖ = 1) (hucont : ContinuousOn u (Metric.closedBall y R))
  (huinterior : ∀ x ∈ Metric.ball y R, ContDiffAt ℝ 2 u x)
  (hderiv : DifferentiableAt ℝ u (y + R • e))
  (hlap : ∀ x ∈ Metric.ball y R, Laplacian.laplacian u x ≤ 0)
  (hmin : ∀ x ∈ Metric.closedBall y R, x ≠ y + R • e → u (y + R • e) < u x) :
  (fderiv ℝ u (y + R • e)) e < 0
Sources
LeanTauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_ball_of_le_sphere · TauCeti.fderiv_pos_of_mul_le_laplacian_add_fderiv_of_lt_ball_of_le_sphere · TauCeti.fderiv_neg_of_laplacian_add_fderiv_le_mul_of_gt_ball_of_ge_sphere · TauCeti.fderiv_pos_of_harmonicOnNhd_of_lt_closedBall · TauCeti.fderiv_neg_of_harmonicOnNhd_of_gt_closedBall · TauCeti.fderiv_pos_of_laplacian_nonneg_of_lt_closedBall · TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_ball_of_ge_sphere · TauCeti.fderiv_neg_of_laplacian_nonpos_of_gt_closedBall
Used by 1
Used byPerron's theorem

TheoremHorn's theorem (LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull)#

Every point d of the convex hull of the rearrangements of the spectrum of a symmetric operator T is the diagonal of T in some orthonormal basis: there is an orthonormal basis e with Re⟪T eₖ, eₖ⟫ = dₖ for every k.

LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} {n : ℕ} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  {d : Fin n → ℝ} (hd : d ∈ (convexHull ℝ) (Set.range fun σ => hT.eigenvalues hn ∘ ⇑σ)) :
  ∃ e, ∀ (k : Fin n), RCLike.re (inner 𝕜 (T (e k)) (e k)) = d k
Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull.

Sources
LeanLinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull
Uses 1 · Used by 2
Proof usesRado's theorem
Used byThe Schur–Horn theorem (LinearMap.IsSymmetric.range_re_inner_apply_self_eq_convexHull_eigenvalues_comp_perm) · Horn's theorem (Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq)

TheoremThe interval/exterior Sylvester bound#

Let A and B be symmetric operators on finite-dimensional inner product spaces. If the eigenvalues of A lie in [a, b] and those of B outside (a - δ, b + δ), then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N. In particular every solution of the Sylvester equation A X - X B = C satisfies δ N(X) ≤ N(C).

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {a b δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  (h : Module.End.PointIntervalExteriorGap ↑A ⊤ ↑B ⊤ a b δ) (X : F →L[𝕜] E) :
  δ * N ↑X ≤ N ↑((A.sylvester B) X)
Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap.

Other forms

The interval/exterior Sylvester bound on invariant subspaces. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_of_mem.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_of_mem.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {a b δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  {S : Submodule 𝕜 E} {T : Submodule 𝕜 F} (hS : ∀ x ∈ S, A x ∈ S) (hT : ∀ y ∈ T, B y ∈ T)
  (h : Module.End.PointIntervalExteriorGap (↑A) S (↑B) T a b δ) {X : F →L[𝕜] E}
  (hXS : ∀ (y : F), X y ∈ S) (hXT : ∀ y ∈ Tᗮ, X y = 0) : δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior Sylvester bound on invariant subspaces, reversed orientation. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap_of_mem.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap_of_mem.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {a b δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  {S : Submodule 𝕜 E} {T : Submodule 𝕜 F} (hS : ∀ x ∈ S, A x ∈ S) (hT : ∀ y ∈ T, B y ∈ T)
  (h : Module.End.PointIntervalExteriorGap (↑B) T (↑A) S a b δ) {X : F →L[𝕜] E}
  (hXS : ∀ (y : F), X y ∈ S) (hXT : ∀ y ∈ Tᗮ, X y = 0) : δ * N ↑X ≤ N ↑((A.sylvester B) X)

The interval/exterior Sylvester bound, reversed orientation. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {a b δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric)
  (h : Module.End.PointIntervalExteriorGap ↑B ⊤ ↑A ⊤ a b δ) (X : F →L[𝕜] E) :
  δ * N ↑X ≤ N ↑((A.sylvester B) X)
Sources
LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap · TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_of_mem · TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap_of_mem · TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_pointIntervalExteriorGap_swap
Uses 2 · Used by 3
Proof usesCourant–Fischer, lower direction · Fan dominance
Used byThe perturbation Davis–Kahan sin Θ theorem · The residual Davis–Kahan sin Θ theorem · The Davis–Kahan sin 2Θ theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.