structure Orthogonalization.FinDim.JointEigenbasis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (x a : H →L[ℂ] H) : Type u_1

A joint orthonormal eigenbasis for a pair of operators x a : H →L[ℂ] H: an orthonormal basis basis of H, indexed by Fin (finrank ℂ H), each of whose vectors is an eigenvector of x with real eigenvalue lam k and an eigenvector of a with real eigenvalue mu k.

Such a datum exists exactly when x and a are commuting self-adjoint operators: see Orthogonalization.FinDim.exists_jointEigenbasis for one direction and JointEigenbasis.isSelfAdjoint_fst, JointEigenbasis.isSelfAdjoint_snd, JointEigenbasis.commute for the other.

• basis : OrthonormalBasis (Fin (Module.finrank ℂ H)) ℂ H

  The orthonormal basis of joint eigenvectors.

• lam : Fin (Module.finrank ℂ H) → ℝ

  The (real) eigenvalues of the first operator x.

• mu : Fin (Module.finrank ℂ H) → ℝ

  The (real) eigenvalues of the second operator a.

• apply_fst (k : Fin (Module.finrank ℂ H)) : x (self.basis k) = ↑(self.lam k) • self.basis k

  basis k is an eigenvector of x for the eigenvalue lam k.

• apply_snd (k : Fin (Module.finrank ℂ H)) : a (self.basis k) = ↑(self.mu k) • self.basis k

  basis k is an eigenvector of a for the eigenvalue mu k.

theorem Orthogonalization.FinDim.exists_jointEigenbasis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (hx : IsSelfAdjoint x) (ha : IsSelfAdjoint a) (hxa : Commute x a) : Nonempty (JointEigenbasis x a)

Simultaneous diagonalization. Two commuting self-adjoint operators on a finite-dimensional complex inner product space admit a joint orthonormal eigenbasis with real eigenvalues.

Elementary consequences of the eigen-equations

theorem Orthogonalization.FinDim.JointEigenbasis.norm_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : ‖J.basis k‖ = 1

theorem Orthogonalization.FinDim.JointEigenbasis.basis_ne_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : J.basis k ≠ 0

theorem Orthogonalization.FinDim.JointEigenbasis.inner_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) : inner ℂ (J.basis k) (J.basis l) = if k = l then 1 else 0

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.inner_basis_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : inner ℂ (J.basis k) (J.basis k) = 1

theorem Orthogonalization.FinDim.JointEigenbasis.ext_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {S T : H →L[ℂ] H} (h : ∀ (k : Fin (Module.finrank ℂ H)), S (J.basis k) = T (J.basis k)) : S = T

Two continuous operators agreeing on the joint eigenbasis are equal.

def Orthogonalization.FinDim.JointEigenbasis.swap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : JointEigenbasis a x

Exchanging the roles of the two operators.

Equations

• J.swap = { basis := J.basis, lam := J.mu, mu := J.lam, apply_fst := ⋯, apply_snd := ⋯ }

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.swap_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : J.swap.basis = J.basis

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.swap_lam {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : J.swap.lam = J.mu

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.swap_mu {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : J.swap.mu = J.lam

The rank-one spectral projections

noncomputable def Orthogonalization.FinDim.JointEigenbasis.P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : H →L[ℂ] H

The orthogonal projection onto the line spanned by the k-th joint eigenvector, i.e. the k-th rank-one spectral projection of the pair.

Equations

• J.P k = (ℂ ∙ J.basis k).starProjection

theorem Orthogonalization.FinDim.JointEigenbasis.P_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (w : H) : (J.P k) w = inner ℂ (J.basis k) w • J.basis k

theorem Orthogonalization.FinDim.JointEigenbasis.P_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : IsStarProjection (J.P k)

Each P k is an orthogonal (star) projection: self-adjoint and idempotent.

theorem Orthogonalization.FinDim.JointEigenbasis.P_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : IsSelfAdjoint (J.P k)

theorem Orthogonalization.FinDim.JointEigenbasis.P_apply_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) : (J.P k) (J.basis l) = if k = l then J.basis k else 0

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.P_apply_basis_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : (J.P k) (J.basis k) = J.basis k

theorem Orthogonalization.FinDim.JointEigenbasis.P_apply_basis_of_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (h : k ≠ l) : (J.P k) (J.basis l) = 0

theorem Orthogonalization.FinDim.JointEigenbasis.P_apply_basis' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) : (J.P k) (J.basis l) = (if l = k then 1 else 0) • J.basis l

A variant of P_apply_basis phrased as a scalar multiple of basis l, convenient for module-style computations.

theorem Orthogonalization.FinDim.JointEigenbasis.P_mul_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (h : k ≠ l) : J.P k * J.P l = 0

Distinct rank-one spectral projections are orthogonal.

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.P_mul_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : J.P k * J.P k = J.P k

theorem Orthogonalization.FinDim.JointEigenbasis.sum_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : ∑ k : Fin (Module.finrank ℂ H), J.P k = 1

The rank-one spectral projections form a resolution of the identity.

Spectral decomposition

theorem Orthogonalization.FinDim.JointEigenbasis.eq_sum_lam_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : x = ∑ k : Fin (Module.finrank ℂ H), ↑(J.lam k) • J.P k

The spectral decomposition of x in its joint eigenbasis.

theorem Orthogonalization.FinDim.JointEigenbasis.eq_sum_mu_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : a = ∑ k : Fin (Module.finrank ℂ H), ↑(J.mu k) • J.P k

The spectral decomposition of a in its joint eigenbasis.

theorem Orthogonalization.FinDim.JointEigenbasis.isSelfAdjoint_fst {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : IsSelfAdjoint x

An operator carrying a joint eigenbasis (with real eigenvalues) is self-adjoint.

theorem Orthogonalization.FinDim.JointEigenbasis.isSelfAdjoint_snd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : IsSelfAdjoint a

The second operator of a joint eigenbasis is self-adjoint.

theorem Orthogonalization.FinDim.JointEigenbasis.commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : Commute x a

Operators sharing a joint eigenbasis commute.

Commutation with the spectral projections

theorem Orthogonalization.FinDim.JointEigenbasis.commute_P_of_eigen {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {T : H →L[ℂ] H} (hT : IsSelfAdjoint T) {k : Fin (Module.finrank ℂ H)} {c : ℝ} (hc : T (J.basis k) = ↑c • J.basis k) : Commute T (J.P k)

A self-adjoint operator having basis k as an eigenvector with a real eigenvalue commutes with the corresponding rank-one projection P k.

theorem Orthogonalization.FinDim.JointEigenbasis.commute_fst_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : Commute x (J.P k)

theorem Orthogonalization.FinDim.JointEigenbasis.commute_snd_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) : Commute a (J.P k)

Trace

theorem Orthogonalization.FinDim.JointEigenbasis.trace_eq_sum_lam {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : (LinearMap.trace ℂ H) ↑x = ∑ k : Fin (Module.finrank ℂ H), ↑(J.lam k)

The trace of x is the sum of its eigenvalues.

theorem Orthogonalization.FinDim.JointEigenbasis.trace_eq_sum_mu {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : (LinearMap.trace ℂ H) ↑a = ∑ k : Fin (Module.finrank ℂ H), ↑(J.mu k)

The trace of a is the sum of its eigenvalues.

The Loewner order and the eigenvalues

theorem Orthogonalization.FinDim.JointEigenbasis.isPositive_sum_smul_P {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {c : Fin (Module.finrank ℂ H) → ℝ} (hc : ∀ (k : Fin (Module.finrank ℂ H)), 0 ≤ c k) : (∑ k : Fin (Module.finrank ℂ H), ↑(c k) • J.P k).IsPositive

A nonnegative combination of the rank-one spectral projections is a positive operator.

theorem Orthogonalization.FinDim.JointEigenbasis.nonneg_of_lam_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (h : ∀ (k : Fin (Module.finrank ℂ H)), 0 ≤ J.lam k) : 0 ≤ x

If all eigenvalues of x are nonnegative then 0 ≤ x in the Loewner order.

theorem Orthogonalization.FinDim.JointEigenbasis.le_one_of_lam_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (h : ∀ (k : Fin (Module.finrank ℂ H)), J.lam k ≤ 1) : x ≤ 1

If all eigenvalues of x are at most 1 then x ≤ 1 in the Loewner order.

theorem Orthogonalization.FinDim.JointEigenbasis.lam_nonneg_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (h : 0 ≤ x) (k : Fin (Module.finrank ℂ H)) : 0 ≤ J.lam k

Conversely, 0 ≤ x forces every eigenvalue of x to be nonnegative.

theorem Orthogonalization.FinDim.JointEigenbasis.lam_le_one_of_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (h : x ≤ 1) (k : Fin (Module.finrank ℂ H)) : J.lam k ≤ 1

Conversely, x ≤ 1 forces every eigenvalue of x to be at most 1.

theorem Orthogonalization.FinDim.JointEigenbasis.mem_Icc_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : 0 ≤ x ∧ x ≤ 1 ↔ ∀ (k : Fin (Module.finrank ℂ H)), J.lam k ∈ Set.Icc 0 1

x is in the operator interval [0, 1] exactly when all its eigenvalues are.

The projections among the operators of a joint eigenbasis

theorem Orthogonalization.FinDim.JointEigenbasis.isStarProjection_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) : IsStarProjection x ↔ ∀ (k : Fin (Module.finrank ℂ H)), J.lam k = 0 ∨ J.lam k = 1

An operator diagonal in an orthonormal basis with real eigenvalues is a star projection exactly when all its eigenvalues are 0 or 1.

Perturbations: moving eigenvalue mass between two basis vectors

These are the operations Lemma 3.1 performs on an extreme point of its convex set: they preserve the joint eigenbasis (hence the commutation with a and the self-adjointness), preserve or shift the trace by a controlled amount, and stay inside [0, 1] as long as the perturbed eigenvalues do.

noncomputable def Orthogonalization.FinDim.JointEigenbasis.shiftPair {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : JointEigenbasis (x + ↑δ • (J.P k - J.P l)) a

Adding δ to the k-th eigenvalue and subtracting δ from the l-th one: the operator x + δ • (P k - P l) is still diagonal in J.basis, and still has a as a joint partner.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : (J.shiftPair k l δ).basis = J.basis

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_mu {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : (J.shiftPair k l δ).mu = J.mu

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_lam {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) (m : Fin (Module.finrank ℂ H)) : (J.shiftPair k l δ).lam m = (J.lam m + if m = k then δ else 0) - if m = l then δ else 0

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_lam_fst {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (hkl : k ≠ l) (δ : ℝ) : (J.shiftPair k l δ).lam k = J.lam k + δ

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_lam_snd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (hkl : k ≠ l) (δ : ℝ) : (J.shiftPair k l δ).lam l = J.lam l - δ

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_lam_of_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l m : Fin (Module.finrank ℂ H)} (hk : m ≠ k) (hl : m ≠ l) (δ : ℝ) : (J.shiftPair k l δ).lam m = J.lam m

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_lam_eq_cases {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (hkl : k ≠ l) (δ : ℝ) (m : Fin (Module.finrank ℂ H)) : (J.shiftPair k l δ).lam m = J.lam k + δ ∨ (J.shiftPair k l δ).lam m = J.lam l - δ ∨ (J.shiftPair k l δ).lam m = J.lam m

Every eigenvalue of the two-sided shift is either one of the two moved ones or an untouched eigenvalue of x.

theorem Orthogonalization.FinDim.JointEigenbasis.commute_shiftPair {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : Commute (x + ↑δ • (J.P k - J.P l)) a

The two-sided shift still commutes with a.

theorem Orthogonalization.FinDim.JointEigenbasis.isSelfAdjoint_shiftPair {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : IsSelfAdjoint (x + ↑δ • (J.P k - J.P l))

The two-sided shift is self-adjoint.

theorem Orthogonalization.FinDim.JointEigenbasis.trace_shiftPair {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) : (LinearMap.trace ℂ H) ↑(x + ↑δ • (J.P k - J.P l)) = (LinearMap.trace ℂ H) ↑x

The two-sided shift preserves the trace.

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_mem_Icc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k l : Fin (Module.finrank ℂ H)) (δ : ℝ) (h0 : ∀ (m : Fin (Module.finrank ℂ H)), 0 ≤ (J.shiftPair k l δ).lam m) (h1 : ∀ (m : Fin (Module.finrank ℂ H)), (J.shiftPair k l δ).lam m ≤ 1) : 0 ≤ x + ↑δ • (J.P k - J.P l) ∧ x + ↑δ • (J.P k - J.P l) ≤ 1

The two-sided shift stays in the operator interval [0, 1] as soon as the shifted eigenvalues do.

theorem Orthogonalization.FinDim.JointEigenbasis.shiftPair_mem_Icc_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k l : Fin (Module.finrank ℂ H)} (hkl : k ≠ l) (δ : ℝ) (h : ∀ (m : Fin (Module.finrank ℂ H)), J.lam m ∈ Set.Icc 0 1) (hk : J.lam k + δ ∈ Set.Icc 0 1) (hl : J.lam l - δ ∈ Set.Icc 0 1) : 0 ≤ x + ↑δ • (J.P k - J.P l) ∧ x + ↑δ • (J.P k - J.P l) ≤ 1

The form in which Lemma 3.1 uses the previous statement: if x already lies in [0, 1] eigenvalue-wise and the two moved eigenvalues stay in [0, 1], then so does the perturbed operator.

noncomputable def Orthogonalization.FinDim.JointEigenbasis.shiftOne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : JointEigenbasis (x + ↑δ • J.P k) a

Adding δ to the k-th eigenvalue only: the operator x + δ • P k is still diagonal in J.basis, and still has a as a joint partner.

Equations

• J.shiftOne k δ = { basis := J.basis, lam := fun (m : Fin (Module.finrank ℂ H)) => J.lam m + if m = k then δ else 0, mu := J.mu, apply_fst := ⋯, apply_snd := ⋯ }

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_basis {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : (J.shiftOne k δ).basis = J.basis

@[simp]

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_mu {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : (J.shiftOne k δ).mu = J.mu

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_lam {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) (m : Fin (Module.finrank ℂ H)) : (J.shiftOne k δ).lam m = J.lam m + if m = k then δ else 0

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_lam_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : (J.shiftOne k δ).lam k = J.lam k + δ

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_lam_of_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) {k m : Fin (Module.finrank ℂ H)} (hk : m ≠ k) (δ : ℝ) : (J.shiftOne k δ).lam m = J.lam m

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_lam_eq_cases {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) (m : Fin (Module.finrank ℂ H)) : (J.shiftOne k δ).lam m = J.lam k + δ ∨ (J.shiftOne k δ).lam m = J.lam m

Every eigenvalue of the one-sided shift is either the moved one or an untouched eigenvalue of x.

theorem Orthogonalization.FinDim.JointEigenbasis.commute_shiftOne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : Commute (x + ↑δ • J.P k) a

The one-sided shift still commutes with a.

theorem Orthogonalization.FinDim.JointEigenbasis.isSelfAdjoint_shiftOne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : IsSelfAdjoint (x + ↑δ • J.P k)

The one-sided shift is self-adjoint.

theorem Orthogonalization.FinDim.JointEigenbasis.trace_shiftOne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) : (LinearMap.trace ℂ H) ↑(x + ↑δ • J.P k) = (LinearMap.trace ℂ H) ↑x + ↑δ

The one-sided shift moves the trace by exactly δ.

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_mem_Icc {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) (h0 : ∀ (m : Fin (Module.finrank ℂ H)), 0 ≤ (J.shiftOne k δ).lam m) (h1 : ∀ (m : Fin (Module.finrank ℂ H)), (J.shiftOne k δ).lam m ≤ 1) : 0 ≤ x + ↑δ • J.P k ∧ x + ↑δ • J.P k ≤ 1

The one-sided shift stays in the operator interval [0, 1] as soon as the shifted eigenvalues do.

theorem Orthogonalization.FinDim.JointEigenbasis.shiftOne_mem_Icc_of {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {x a : H →L[ℂ] H} (J : JointEigenbasis x a) (k : Fin (Module.finrank ℂ H)) (δ : ℝ) (h : ∀ (m : Fin (Module.finrank ℂ H)), J.lam m ∈ Set.Icc 0 1) (hk : J.lam k + δ ∈ Set.Icc 0 1) : 0 ≤ x + ↑δ • J.P k ∧ x + ↑δ • J.P k ≤ 1

The form in which Lemma 3.1 uses the previous statement.