JointBasis.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

An orthonormal eigenbasis for a commuting symmetric family

This is the finite-dimensional simultaneous spectral step in the completion argument. It specializes mathlib's joint-eigenspace decomposition and retains an explicit common eigenvalue for each basis vector and each operator.

abbrev OAI.MUB6.Weiner.JointIndex line 22
Source documentation
Finite tuples of actual eigenvalues, excluding irrelevant scalar tuples.
```
abbrev JointIndex (T : ι → End ℂ E) := ∀ i, (T i).Eigenvalues
```
def OAI.MUB6.Weiner.jointSubspace line 24
lemma OAI.MUB6.Weiner.jointSubspace_span line 28
lemma OAI.MUB6.Weiner.jointSubspace_orthogonal line 42

theorem OAI.MUB6.Weiner.exists_joint_eigenbasis line 53

Source documentation

A finite commuting family of symmetric complex linear operators admits a single orthonormal basis of simultaneous eigenvectors.

theorem exists_joint_eigenbasis (T : ι → End ℂ E)
    (hsym : ∀ i, (T i).IsSymmetric) (hcomm : Pairwise (Commute on T)) :
    ∃ (b : OrthonormalBasis (Fin (finrank ℂ E)) ℂ E)
      (ev : Fin (finrank ℂ E) → ι → ℂ),
      ∀ j i, T i (b j) = ev j i • b j := by
…

theorem OAI.MUB6.Weiner.commute_rankOne_of_eigenbasis line 74

Source documentation

Every coordinate projection of an eigenbasis commutes with the operator. This argument only uses the basis expansions, so no separate claim about the reality of the eigenvalues is needed.

theorem commute_rankOne_of_eigenbasis {κ : Type*} [Fintype κ]
    (b : OrthonormalBasis κ ℂ E) (T : End ℂ E) (ev : κ → ℂ)
    (heig : ∀ j, T (b j) = ev j • b j) (i : κ) :
    Commute T (InnerProductSpace.rankOne ℂ (b i) (b i)).toLinearMap := by
…

theorem OAI.MUB6.Weiner.exists_joint_projection_basis line 91

Source documentation

The simultaneous eigenbasis can equivalently be characterized by its commuting rank-one coordinate projections.

theorem exists_joint_projection_basis (T : ι → End ℂ E)
    (hsym : ∀ i, (T i).IsSymmetric) (hcomm : Pairwise (Commute on T)) :
    ∃ b : OrthonormalBasis (Fin (finrank ℂ E)) ℂ E,
      ∀ i j, Commute (T i) (InnerProductSpace.rankOne ℂ (b j) (b j)).toLinearMap := by
…