Matrix

Results named in Tau Ceti's TauCeti.Analysis.Matrix modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe 2 × 2 Schur–Horn theorem#

For l₂ ≤ l₁, a real symmetric 2 × 2 matrix with diagonal (d₁, d₂) and characteristic polynomial (X - l₁) (X - l₂) exists exactly when (d₁, d₂) is majorized by (l₁, l₂), that is, when l₂ ≤ d₁ ≤ l₁ and d₁ + d₂ = l₁ + l₂. In that case !![d₁, b; b, d₂] with b = √((l₁ - d₁) (d₁ - l₂)) is such a matrix.

Matrix.exists_isSymm_fin_two_charpoly_eq_iff {l₁ l₂ d₁ d₂ : ℝ} (hl : l₂ ≤ l₁) :
  (∃ A,
      A.IsSymm ∧
        A 0 0 = d₁ ∧
          A 1 1 = d₂ ∧
            A.charpoly = (Polynomial.X - Polynomial.C l₁) * (Polynomial.X - Polynomial.C l₂)) ↔
    l₂ ≤ d₁ ∧ d₁ ≤ l₁ ∧ d₁ + d₂ = l₁ + l₂
Lean

Formalized in Tau Ceti as Matrix.exists_isSymm_fin_two_charpoly_eq_iff.

Sources
LeanMatrix.exists_isSymm_fin_two_charpoly_eq_iff

TheoremGrothendieck's inequality over the reals, with constant κ_ℝ = 8#

if |∑ i, ∑ j, a i j * s i * t j| ≤ C for all real scalars of absolute value at most one, then |∑ i, ∑ j, a i j * ⟪u i, v j⟫| ≤ 8 * C for all families of vectors of norm at most one in any real inner product space.

Matrix.abs_sum_sum_mul_inner_le_eight_mul.{u_1, u_2, u_3} {ι : Type u_1} {κ : Type u_2} [Fintype ι]
  [Fintype κ] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : Matrix ι κ ℝ)
  {C : ℝ}
  (h :
    ∀ (s : ι → ℝ) (t : κ → ℝ),
      (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i, ∑ j, a i j * s i * t j| ≤ C)
  {u : ι → E} {v : κ → E} (hu : ∀ (i : ι), ‖u i‖ ≤ 1) (hv : ∀ (j : κ), ‖v j‖ ≤ 1) :
  |∑ i, ∑ j, a i j * inner ℝ (u i) (v j)| ≤ 8 * C
Lean

Formalized in Tau Ceti as Matrix.abs_sum_sum_mul_inner_le_eight_mul.

Other forms

Grothendieck's inequality in terms of Γ(a) = Matrix.innerProductSup a. Formalized in Tau Ceti as Matrix.innerProductSup_le_eight_mul.

Matrix.innerProductSup_le_eight_mul.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ]
  (a : Matrix ι κ ℝ) {C : ℝ}
  (h :
    ∀ (s : ι → ℝ) (t : κ → ℝ),
      (∀ (i : ι), |s i| ≤ 1) → (∀ (j : κ), |t j| ≤ 1) → |∑ i, ∑ j, a i j * s i * t j| ≤ C) :
  a.innerProductSup ≤ 8 * C

Grothendieck's inequality over an RCLike field, with constant κ_𝕜 = 16. Formalized in Tau Ceti as Matrix.norm_sum_sum_mul_inner_le_sixteen_mul.

Matrix.norm_sum_sum_mul_inner_le_sixteen_mul.{u_1, u_2, u_3, u_4} {ι : Type u_1} {κ : Type u_2}
  [Fintype ι] [Fintype κ] {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] (a : Matrix ι κ 𝕜) {C : ℝ}
  (h :
    ∀ (s : ι → 𝕜) (t : κ → 𝕜),
      (∀ (i : ι), ‖s i‖ ≤ 1) → (∀ (j : κ), ‖t j‖ ≤ 1) → ‖∑ i, ∑ j, a i j * s i * t j‖ ≤ C)
  {u : ι → E} {v : κ → E} (hu : ∀ (i : ι), ‖u i‖ ≤ 1) (hv : ∀ (j : κ), ‖v j‖ ≤ 1) :
  ‖∑ i, ∑ j, a i j * inner 𝕜 (u i) (v j)‖ ≤ 16 * C
Sources
LeanMatrix.abs_sum_sum_mul_inner_le_eight_mul · Matrix.innerProductSup_le_eight_mul · Matrix.norm_sum_sum_mul_inner_le_sixteen_mul
Used by 2
Used byGrothendieck's theorem · Grothendieck's inequality

TheoremHadamard--Fischer inequality#

The determinant of a positive-semidefinite block matrix is at most the product of the diagonal-block determinants.

Matrix.PosSemidef.det_fromBlocks_le.{u_1, u_2, u_3} {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3}
  [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {A : Matrix m m 𝕜}
  {B : Matrix m n 𝕜} {D : Matrix n n 𝕜} (h : (Matrix.fromBlocks A B B.conjTranspose D).PosSemidef) :
  (Matrix.fromBlocks A B B.conjTranspose D).det ≤ A.det * D.det
Lean

Formalized in Tau Ceti as Matrix.PosSemidef.det_fromBlocks_le.

Sources
LeanMatrix.PosSemidef.det_fromBlocks_le
Used by 1
Used byKoteljanskii's inequality for overlapping blocks

TheoremThe Hoffman–Wielandt inequality for Hermitian matrices#

the squared Euclidean distance between the decreasingly sorted spectra is at most the squared Frobenius norm ‖A - B‖_F².

Matrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq.{u_1, u_2} {n : Type u_1}
  {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A B : Matrix n n 𝕜} (hA : A.IsHermitian)
  (hB : B.IsHermitian) : ∑ i, (hA.eigenvalues₀ i - hB.eigenvalues₀ i) ^ 2 ≤ ‖A - B‖ ^ 2
Lean

Formalized in Tau Ceti as Matrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq.

Sources
LeanMatrix.IsHermitian.sum_sq_eigenvalues₀_sub_le_frobenius_norm_sub_sq
Uses 1 · Used by 1
Proof usesThe Hoffman–Wielandt inequality
Used bySpectral Wasserstein bound, squared form

TheoremHorn's theorem (Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq)#

Every point d of the convex hull of the rearrangements of w is the diagonal of U diag(w) Uᴴ for some unitary U.

Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq.{u_1, u_2} {𝕜 : Type u_1}
  {ι : Type u_2} [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {w d : ι → ℝ}
  (hd : d ∈ (convexHull ℝ) (Set.range fun σ => w ∘ ⇑σ)) :
  ∃ U ∈ Matrix.unitaryGroup ι 𝕜,
    ∀ (k : ι), RCLike.re (((U * Matrix.diagonal fun i => ↑(w i)) * star U) k k) = d k
Lean

Formalized in Tau Ceti as Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq.

Sources
LeanMatrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq
Uses 1 · Used by 1
Proof usesHorn's theorem (LinearMap.IsSymmetric.exists_orthonormalBasis_re_inner_apply_self_eq_of_mem_convexHull)
Used byThe Schur–Horn theorem (Matrix.range_re_diag_unitary_mul_diagonal_mul_star)

TheoremJensen's operator inequality for isometries#

Let f be operator concave on a set S of matrices closed under unitary conjugation, in the sense that A ↦ cfc f A is concave on S. For a Hermitian A ∈ S and an isometry V, that is Vᴴ * V = 1, compressing by V lowers the functional calculus: Vᴴ * cfc f A * V ≤ cfc f (Vᴴ * A * V).

Matrix.conjTranspose_mul_cfc_mul_le_cfc_conjTranspose_mul_mul.{u_1, u_2, u_3} {m : Type u_1}
  {n : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
  {f : ℝ → ℝ} {S : Set (Matrix m m 𝕜)} (hf : ConcaveOn ℝ S (cfc f))
  (hS : ∀ a ∈ S, ∀ u ∈ unitary (Matrix m m 𝕜), u * a * star u ∈ S) {A : Matrix m m 𝕜} (hAS : A ∈ S)
  (hA : A.IsHermitian) {V : Matrix m n 𝕜} (hV : V.conjTranspose * V = 1) :
  V.conjTranspose * cfc f A * V ≤ cfc f (V.conjTranspose * A * V)
Lean

Formalized in Tau Ceti as Matrix.conjTranspose_mul_cfc_mul_le_cfc_conjTranspose_mul_mul.

Sources
LeanMatrix.conjTranspose_mul_cfc_mul_le_cfc_conjTranspose_mul_mul

TheoremKlein's inequality for the relative entropy#

For positive semidefinite ρ and σ, Tr ρ - Tr σ ≤ D(ρ ‖ σ).

Matrix.PosSemidef.re_trace_sub_trace_le_relativeEntropy.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜]
  {n : Type u_2} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n 𝕜} (hρ : ρ.PosSemidef)
  (hσ : σ.PosSemidef) : ↑(RCLike.re (ρ.trace - σ.trace)) ≤ ρ.relativeEntropy σ
Lean

Formalized in Tau Ceti as Matrix.PosSemidef.re_trace_sub_trace_le_relativeEntropy.

Sources
LeanMatrix.PosSemidef.re_trace_sub_trace_le_relativeEntropy

TheoremKoteljanskii's inequality for overlapping blocks#

The product of the principal minors on the common block and on all three blocks is bounded by the product of the two intermediate principal minors. No block need be nonsingular.

Matrix.PosSemidef.det_mul_det_fromBlocks_le.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {m : Type u_2}
  {n : Type u_3} {p : Type u_4} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
  [Fintype p] [DecidableEq p] {A : Matrix m m 𝕜} {B : Matrix m n 𝕜} {C : Matrix m p 𝕜}
  {D : Matrix n n 𝕜} {E : Matrix n p 𝕜} {F : Matrix p p 𝕜}
  (h :
    (Matrix.fromBlocks A (B.fromCols C) (B.fromCols C).conjTranspose
        (Matrix.fromBlocks D E E.conjTranspose F)).PosSemidef) :
  A.det *
      (Matrix.fromBlocks A (B.fromCols C) (B.fromCols C).conjTranspose
          (Matrix.fromBlocks D E E.conjTranspose F)).det ≤
    (Matrix.fromBlocks A B B.conjTranspose D).det * (Matrix.fromBlocks A C C.conjTranspose F).det
Lean

Formalized in Tau Ceti as Matrix.PosSemidef.det_mul_det_fromBlocks_le.

Sources
LeanMatrix.PosSemidef.det_mul_det_fromBlocks_le
Uses 1
Proof usesHadamard--Fischer inequality

TheoremMinkowski's determinant inequality#

For positive semidefinite real n × n matrices A and B with n ≥ 1, det A ^ (1 / n) + det B ^ (1 / n) ≤ det (A + B) ^ (1 / n).

Matrix.PosSemidef.det_rpow_add_det_rpow_le.{u_1} {n : Type u_1} [Fintype n] [DecidableEq n]
  [Nonempty n] {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) :
  A.det ^ (↑(Fintype.card n))⁻¹ + B.det ^ (↑(Fintype.card n))⁻¹ ≤
    (A + B).det ^ (↑(Fintype.card n))⁻¹
Lean

Formalized in Tau Ceti as Matrix.PosSemidef.det_rpow_add_det_rpow_le.

Other forms

Minkowski's determinant inequality for positive operators. Formalized in Tau Ceti as LinearMap.IsPositive.det_rpow_add_det_rpow_le.

LinearMap.IsPositive.det_rpow_add_det_rpow_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {A B : E →ₗ[ℝ] E}
  (hA : A.IsPositive) (hB : B.IsPositive) :
  LinearMap.det A ^ (↑(Module.finrank ℝ E))⁻¹ + LinearMap.det B ^ (↑(Module.finrank ℝ E))⁻¹ ≤
    LinearMap.det (A + B) ^ (↑(Module.finrank ℝ E))⁻¹
Sources
LeanMatrix.PosSemidef.det_rpow_add_det_rpow_le · LinearMap.IsPositive.det_rpow_add_det_rpow_le
Used by 1
Used byMcCann's displacement convexity of internal energies

TheoremRow Hodge lower bound for the principal-minor series#

Let v be a real additive valuation with ‖x‖ = b ^ (-v x) for x ≠ 0, where b > 1. For a bounded row majorant ‖A i j‖ ≤ r i, the row Hodge polygon of r lies below the Newton polygon of the principal-minor series A.charPowerSeries, which is the Fredholm determinant det (1 - T A) when its principal-minor families are summable.

Matrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries.{u_1, u_2} {ι : Type u_1} {K : Type u_2}
  [DecidableEq ι] [NormedField K] [IsUltrametricDist K] {v : AddValuation K (WithTop ℝ)} {b : ℝ}
  {A : Matrix ι ι K} {r : ι → ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀))
  (hr : BddAbove (Set.range r)) (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) :
  TauCeti.rowHodgePolygon b r ≤ A.charPowerSeries.newtonPolygon v
Lean

Formalized in Tau Ceti as Matrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries.

Sources
LeanMatrix.rowHodgePolygon_le_newtonPolygon_charPowerSeries
Used by 1
Used byRow Hodge lower bound for a row-compact operator

TheoremSchur's theorem (Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull)#

For a unitary U, the diagonal of U diag(w) Uᴴ lies in the convex hull of the rearrangements w ∘ σ of w.

Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2}
  [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {U : Matrix ι ι 𝕜} (hU : U ∈ Matrix.unitaryGroup ι 𝕜)
  (w : ι → ℝ) :
  (fun k => RCLike.re (((U * Matrix.diagonal fun i => ↑(w i)) * star U) k k)) ∈
    (convexHull ℝ) (Set.range fun σ => w ∘ ⇑σ)
Lean

Formalized in Tau Ceti as Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull.

Sources
LeanMatrix.re_diag_mul_diagonal_mul_star_mem_convexHull
Used by 1
Used byThe Schur–Horn theorem (Matrix.range_re_diag_unitary_mul_diagonal_mul_star)

TheoremThe Schur–Horn theorem (Matrix.range_re_diag_unitary_mul_diagonal_mul_star)#

The diagonals of the matrices U diag(w) Uᴴ, for U unitary, form exactly the convex hull of the rearrangements of w. In the language of moment maps: the image of the unitary orbit of diag(w) under the moment map of the diagonal torus is the permutohedron of w.

Matrix.range_re_diag_unitary_mul_diagonal_mul_star.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2}
  [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (w : ι → ℝ) :
  (Set.range fun U k => RCLike.re (((↑U * Matrix.diagonal fun i => ↑(w i)) * ↑(star U)) k k)) =
    (convexHull ℝ) (Set.range fun σ => w ∘ ⇑σ)
Lean

Formalized in Tau Ceti as Matrix.range_re_diag_unitary_mul_diagonal_mul_star.

Other forms

The Schur–Horn theorem for a Hermitian matrix. Formalized in Tau Ceti as Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star.

Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2}
  [RCLike 𝕜] [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
  (Set.range fun U k => RCLike.re ((↑U * A * ↑(star U)) k k)) =
    (convexHull ℝ) (Set.range fun σ => hA.eigenvalues ∘ ⇑σ)

The Schur–Horn theorem in rank at most one. Formalized in Tau Ceti as Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star.

Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2}
  [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (i₀ : ι) (c : ℝ) :
  (Set.range fun U k =>
      RCLike.re (((↑U * Matrix.diagonal fun i => ↑(Pi.single i₀ c i)) * ↑(star U)) k k)) =
    (convexHull ℝ) (Set.range fun i => Pi.single i c)
Sources
LeanMatrix.range_re_diag_unitary_mul_diagonal_mul_star · Matrix.IsHermitian.range_re_diag_unitary_mul_mul_star · Matrix.range_re_diag_unitary_mul_diagonal_single_mul_star
Uses 2
Proof usesHorn's theorem (Matrix.exists_mem_unitaryGroup_re_diag_mul_diagonal_mul_star_eq) · Schur's theorem (Matrix.re_diag_mul_diagonal_mul_star_mem_convexHull)

TheoremThe singular-value Hoffman–Wielandt inequality for same-shaped rectangular matrices#

the squared distance between their ordered singular values, summed up to the smaller dimension, is bounded by the squared Frobenius norm of their difference.

Matrix.sum_sq_singularValues_toEuclideanLin_sub_le_frobenius_norm_sub_sq.{u_3, u_4, u_5}
  {m : Type u_3} {n : Type u_4} [Fintype m] [Fintype n] [DecidableEq n] {𝕜 : Type u_5} [RCLike 𝕜]
  (A B : Matrix m n 𝕜) :
  ∑ i,
      ((Matrix.toEuclideanLin A).singularValues ↑i - (Matrix.toEuclideanLin B).singularValues ↑i) ^
        2 ≤
    ‖A - B‖ ^ 2
Lean

Formalized in Tau Ceti as Matrix.sum_sq_singularValues_toEuclideanLin_sub_le_frobenius_norm_sub_sq.

Sources
LeanMatrix.sum_sq_singularValues_toEuclideanLin_sub_le_frobenius_norm_sub_sq
Uses 1
Proof usesThe singular-value Hoffman–Wielandt inequality

TheoremThe spectral theorem for normal matrices#

A normal complex matrix is unitarily diagonalizable: there is a unitary matrix U with star U * A * U diagonal.

Matrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal.{u_1} {n : Type u_1} [Fintype n]
  [DecidableEq n] (A : Matrix n n ℂ) [IsStarNormal A] :
  ∃ U ∈ Matrix.unitaryGroup n ℂ, ∃ d, star U * A * U = Matrix.diagonal d
Lean

Formalized in Tau Ceti as Matrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal.

Sources
LeanMatrix.exists_mem_unitaryGroup_star_mul_mul_eq_diagonal
Used by 1
Used byThe Gelfand–Tsetlin decomposition

TheoremSpectral Wasserstein bound, squared form#

The squared W₂ distance between the empirical spectral measures is at most the normalized squared Frobenius distance.

Matrix.wassersteinEDist_two_spectralMeasure_sq_le.{u_1, u_2} {n : Type u_1} {𝕜 : Type u_2}
  [Fintype n] [DecidableEq n] [Nonempty n] [RCLike 𝕜] (A B : Matrix n n 𝕜) (hA : A.IsHermitian)
  (hB : B.IsHermitian) :
  TauCeti.wassersteinEDist 2 ↑(A.spectralMeasure hA) ↑(B.spectralMeasure hB) ^ 2 ≤
    ENNReal.ofReal (‖A - B‖ ^ 2 / ↑(Fintype.card n))
Lean

Formalized in Tau Ceti as Matrix.wassersteinEDist_two_spectralMeasure_sq_le.

Sources
LeanMatrix.wassersteinEDist_two_spectralMeasure_sq_le
Uses 1
Proof usesThe Hoffman–Wielandt inequality for Hermitian matrices

TheoremSylvester's law of inertia for Hermitian matrices#

The signature is unchanged by *-congruence A ↦ P * A * Pᴴ with P invertible.

Matrix.IsHermitian.signature_congr.{u_1, u_3} {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜]
  {A : Matrix ι ι 𝕜} [DecidableEq ι] {P : Matrix ι ι 𝕜} (hP : IsUnit P.det) (hA : A.IsHermitian) :
  ⋯.signature = hA.signature
Lean

Formalized in Tau Ceti as Matrix.IsHermitian.signature_congr.

Sources
LeanMatrix.IsHermitian.signature_congr

TheoremWeyl's additive inequality for Hermitian matrices, upper form#

if i + j ≤ k, then λₖ(A + B) ≤ λᵢ(A) + λⱼ(B) for the decreasing enumerations eigenvalues₀. For k = i + j this is the classical λ_{i+j-1}(A + B) ≤ λᵢ(A) + λⱼ(B) in one-based indexing.

Matrix.IsHermitian.eigenvalues₀_add_le.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜]
  [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian)
  {i j k : Fin (Fintype.card ι)} (hk : ↑i + ↑j ≤ ↑k) :
  ⋯.eigenvalues₀ k ≤ hA.eigenvalues₀ i + hB.eigenvalues₀ j
Lean

Formalized in Tau Ceti as Matrix.IsHermitian.eigenvalues₀_add_le.

Other forms

Weyl's additive inequality for Hermitian matrices, lower form. Formalized in Tau Ceti as Matrix.IsHermitian.le_eigenvalues₀_add.

Matrix.IsHermitian.le_eigenvalues₀_add.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜]
  [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian)
  {i j k : Fin (Fintype.card ι)} (hk : ↑k + Fintype.card ι ≤ ↑i + ↑j + 1) :
  hA.eigenvalues₀ i + hB.eigenvalues₀ j ≤ ⋯.eigenvalues₀ k
Sources
LeanMatrix.IsHermitian.eigenvalues₀_add_le · Matrix.IsHermitian.le_eigenvalues₀_add
Uses 1
Proof usesWeyl's additive inequality, upper form

TheoremWeyl's perturbation bound for ordered eigenvalues of Hermitian matrices#

corresponding eigenvalues differ by at most the Euclidean operator norm of the matrix difference.

Matrix.IsHermitian.abs_eigenvalues₀_sub_le_norm.{u_1, u_2} {𝕜 : Type u_1} {ι : Type u_2} [RCLike 𝕜]
  [Fintype ι] [DecidableEq ι] {A B : Matrix ι ι 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian)
  (i : Fin (Fintype.card ι)) : |hA.eigenvalues₀ i - hB.eigenvalues₀ i| ≤ ‖A - B‖
Lean

Formalized in Tau Ceti as Matrix.IsHermitian.abs_eigenvalues₀_sub_le_norm.

Sources
LeanMatrix.IsHermitian.abs_eigenvalues₀_sub_le_norm
Uses 1
Proof usesWeyl's inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.