orthogonalFamily_eigenspace_inf_eigenspace

English

The joint eigenspaces of a pair of symmetric operators form an orthogonal family.

Русский

Совместные собственные пространства пары симметричных операторов образуют ортогональную семью.

LaTeX

$$$\text{OrthogonalFamily}(\cdot, \text{eigenspaces})$ for symmetric operators$$

Lean4

/-- The joint eigenspaces of a pair of symmetric operators form an
`OrthogonalFamily`. -/
theorem orthogonalFamily_eigenspace_inf_eigenspace (hA : A.IsSymmetric) (hB : B.IsSymmetric) :
    OrthogonalFamily 𝕜 (fun (i : 𝕜 × 𝕜) => (eigenspace A i.2 ⊓ eigenspace B i.1 : Submodule 𝕜 E)) fun i =>
      (eigenspace A i.2 ⊓ eigenspace B i.1).subtypeₗᵢ :=
  OrthogonalFamily.of_pairwise fun i j hij v ⟨hv1, hv2⟩ ↦
    by
    obtain (h₁ | h₂) : i.1 ≠ j.1 ∨ i.2 ≠ j.2 := by rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij
    all_goals intro w ⟨hw1, hw2⟩
    · exact hB.orthogonalFamily_eigenspaces.pairwise h₁ hv2 w hw2
    · exact hA.orthogonalFamily_eigenspaces.pairwise h₂ hv1 w hw1

Похожие утверждения