Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint

Imports

/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Bornemann, Gregory J. Loges
-/
module

public import Physlib.QuantumMechanics.Operators.SpectralTheory.Symmetric

Spectral theory for self-adjoint operators

i. Overview

In this module we develop the spectral theory for self-adjoint operators.

ii. Key results

resolventSet_eq_regularityDomain : The resolvent set and regularity domain coincide. That is, if T - z • 1 has a continuous (equivalently, bounded) inverse then its range is all of H.

mem_resolventSet_of_im_ne_zero : every non-real z lies in the resolvent set of a self-adjoint operator.

sub_smul_surjective : A self-adjoint T has T - z • 1 surjective for every non-real z (in particular T ± i • 1 are onto).

spectrum_real : The spectrum of a self-adjoint unbounded operator is real.

unitaryConj_isSelfAdjoint : Unitary conjugation preserves self-adjointness.

iii. Table of contents

A. Resolvent set

B. Spectrum

C. Unitary conjugation

iv. References

@[expose] public sectioninclude hT

A. Resolvent set



lemma resolventSet_eq_regularityDomain : ρ T = T.regularityDomain := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ ρ T = T.regularityDomain
  refine Subset.antisymm T.resolventSet_subset_regularityDomain fun z hz ↦ ?_H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomain⊢ z ∈ ρ T
  obtain ⟨h_ker, h_cont⟩ := mem_regularityDomain_iff.mp hzH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)⊢ z ∈ ρ T
  refine ⟨h_ker, ?_, h_cont⟩H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)⊢ (T - z • 1).toFun.range = ⊤
  have h_ker' : (T - conj z • 1).toFun.ker = ⊥ := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ ρ T = T.regularityDomainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤
    by_cases hz' : conj z = zposH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)hz':(starRingEnd ℂ) z = z⊢ (T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥negH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)hz':¬(starRingEnd ℂ) z = z⊢ (T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤
    ·posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)hz':(starRingEnd ℂ) z = z⊢ (T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤ exact hz'.symm ▸ h_kerAll goals completed! 🐙H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤
    ·negH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)hz':¬(starRingEnd ℂ) z = z⊢ (T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤ exact (mem_regularityDomain_iff.mp <| (isSymmetric hT).mem_regularityDomain_of_im_ne_zero
        (byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)hz':¬(starRingEnd ℂ) z = z⊢ ((starRingEnd ℂ) z).im ≠ 0H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤ simp_all [Complex.conj_eq_iff_im]All goals completed! 🐙H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤)).1H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.range = ⊤
  have h_orthog := (isUnbounded hT).orthogonal_adjoint_sub_ker hzH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T† - (starRingEnd ℂ) z • 1).domain.subtype (T† - (starRingEnd ℂ) z • 1).toFun.ker)ᗮ =
  (T.closure - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤
  rw [isSelfAdjoint_def.mp hT,H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype (T - (starRingEnd ℂ) z • 1).toFun.ker)ᗮ =
  (T.closure - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype ⊥)ᗮ = (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤ (isClosed hT).closure_eq,H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype (T - (starRingEnd ℂ) z • 1).toFun.ker)ᗮ =
  (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype ⊥)ᗮ = (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤ h_ker'H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype ⊥)ᗮ = (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype ⊥)ᗮ = (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤] at h_orthogH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z ∈ T.regularityDomainh_ker:(T - z • 1).toFun.ker = ⊥h_cont:Continuous ↑(𝑅 T z)h_ker':(T - (starRingEnd ℂ) z • 1).toFun.ker = ⊥h_orthog:(Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype ⊥)ᗮ = (T - z • 1).toFun.range⊢ (T - z • 1).toFun.range = ⊤
  simp [← h_orthog]All goals completed! 🐙

Every non-real z lies in the resolvent set of a self-adjoint operator.


lemma mem_resolventSet_of_im_ne_zero {z : ℂ} (hz : z.im ≠ 0) : z ∈ ρ T := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z.im ≠ 0⊢ z ∈ ρ T
  rw [resolventSet_eq_regularityDomain hTH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z.im ≠ 0⊢ z ∈ T.regularityDomainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z.im ≠ 0⊢ z ∈ T.regularityDomain]H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂhz:z.im ≠ 0⊢ z ∈ T.regularityDomain
  exact (isSymmetric hT).mem_regularityDomain_of_im_ne_zero hzAll goals completed! 🐙

A self-adjoint operator has T - z • 1 surjective for every non-real z: off the real axis a self-adjoint operator has z in its resolvent set, so T - z • 1 has full range.

lemma sub_smul_surjective {z : ℂ} (hz : z.im ≠ 0) : Function.Surjective (T - z • 1).toFun :=
  LinearMap.range_eq_top.mp (mem_resolventSet_iff.mp (mem_resolventSet_of_im_ne_zero hT hz)).2.1

(T - z • 1).range = ⊤ is a sufficient condition for z ∈ ρ T (and it is a necessary condition by definition of ρ).


lemma mem_resolventSet_of_range_eq_top {z : ℂ} (h : (T - z • 1).toFun.range = ⊤) : z ∈ ρ T := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤⊢ z ∈ ρ T
  by_cases hz_im : z.im = 0posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ z ∈ ρ TnegH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:¬z.im = 0⊢ z ∈ ρ T
  ·posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ z ∈ ρ T rw [(isClosed hT).resolventSet_eqposH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ z ∈ {z | (T - z • 1).toFun.ker = ⊥ ∧ (T - z • 1).toFun.range = ⊤}posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ z ∈ {z | (T - z • 1).toFun.ker = ⊥ ∧ (T - z • 1).toFun.range = ⊤}]posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ z ∈ {z | (T - z • 1).toFun.ker = ⊥ ∧ (T - z • 1).toFun.range = ⊤}
    refine ⟨?_, h⟩posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0⊢ (T - z • 1).toFun.ker = ⊥
    have h_orthog := (isUnbounded hT).orthogonal_closure_sub_range zposH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T.closure - z • 1).toFun.rangeᗮ =
  Submodule.map (T† - (starRingEnd ℂ) z • 1).domain.subtype (T† - (starRingEnd ℂ) z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥
    rwa [isSelfAdjoint_def.mp hT,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T.closure - z • 1).toFun.rangeᗮ =
  Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype (T - (starRingEnd ℂ) z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥ (isClosed hT).closure_eq,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.rangeᗮ =
  Submodule.map (T - (starRingEnd ℂ) z • 1).domain.subtype (T - (starRingEnd ℂ) z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥ conj_eq_iff_im.mpr hz_im,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.rangeᗮ = Submodule.map (T - z • 1).domain.subtype (T - z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥ h,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:⊤ᗮ = Submodule.map (T - z • 1).domain.subtype (T - z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥
      Submodule.top_orthogonal_eq_bot,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:⊥ = Submodule.map (T - z • 1).domain.subtype (T - z • 1).toFun.ker⊢ (T - z • 1).toFun.ker = ⊥ Eq.comm,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:Submodule.map (T - z • 1).domain.subtype (T - z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.ker = ⊥ ← LinearMap.le_ker_iff_map,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.ker ≤ (T - z • 1).domain.subtype.ker⊢ (T - z • 1).toFun.ker = ⊥ Submodule.ker_subtype,posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.ker ≤ ⊥⊢ (T - z • 1).toFun.ker = ⊥
      le_bot_iffposH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.ker = ⊥]posH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:z.im = 0h_orthog:(T - z • 1).toFun.ker = ⊥⊢ (T - z • 1).toFun.ker = ⊥ at h_orthog
  ·negH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint Tz:ℂh:(T - z • 1).toFun.range = ⊤hz_im:¬z.im = 0⊢ z ∈ ρ T exact mem_resolventSet_of_im_ne_zero hT hz_imAll goals completed! 🐙

B. Spectrum

The spectrum of a self-adjoint operator is real.


lemma spectrum_real : σ T ⊆ range ofReal := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ σ T ⊆ range ofReal
  rw [spectrum_eq,H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ (ρ T)ᶜ ⊆ range ofRealH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ T.regularityDomainᶜ ⊆ range ofReal resolventSet_eq_regularityDomain hTH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ T.regularityDomainᶜ ⊆ range ofRealH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ T.regularityDomainᶜ ⊆ range ofReal]H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HT:H →ₗ.[ℂ] HhT:IsSelfAdjoint T⊢ T.regularityDomainᶜ ⊆ range ofReal
  exact compl_subset_comm.mp (isSymmetric hT).compl_ofReal_subset_regularityDomainAll goals completed! 🐙

The residual spectrum of a self-adjoint operator is empty.

lemma residualSpectrum_eq_empty : σʳ T = ∅ :=
  eq_empty_iff_forall_notMem.mpr fun _ hz ↦ T.residualSpectrum_subset_spectrum hz
    (resolventSet_eq_regularityDomain hT ▸ T.residualSpectrum_subset_regularityDomain hz)

C. Unitary conjugation

Unitary conjugation preserves self-adjointness: if A is a self-adjoint operator on H and u : H ≃ₗᵢ[ℂ] H' is unitary, then u A u⁻¹ is self-adjoint on H'. Symmetry, dense domain, and the two deficiency surjectivities of A all transfer through u.


lemma unitaryConj_isSelfAdjoint (u : H ≃ₗᵢ[ℂ] H') {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) :
    IsSelfAdjoint (A.unitaryConj u) := byH:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint A⊢ IsSelfAdjoint (unitaryConj u A)
  have hrange {z : ℂ} (hz : z.im ≠ 0) : (A.unitaryConj u - z • 1).toFun.range = ⊤ :=
    LinearMap.range_eq_top.mpr
      (unitaryConj_sub_smul_surjective (IsSelfAdjoint.sub_smul_surjective hA hz))H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ IsSelfAdjoint (unitaryConj u A)
  refine IsSymmetric.isSelfAdjoint_of_range_eq_top
    (IsFormalAdjoint.unitaryConj (IsSelfAdjoint.isSymmetric hA))
    (HasDenseDomain.unitaryConj_dense_domain (IsSelfAdjoint.dense_domain hA)) ?_ ?_refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ (unitaryConj u A + I • 1).toFun.range = ⊤refine_2H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ (unitaryConj u A - I • 1).toFun.range = ⊤
  ·refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ (unitaryConj u A + I • 1).toFun.range = ⊤ have hI : A.unitaryConj u + I • 1 = A.unitaryConj u - (-I) • 1 :=
      LinearPMap.ext rfl fun x hf hg => byH:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤x:H'hf:x ∈ (unitaryConj u A + I • 1).domainhg:x ∈ (unitaryConj u A - -I • 1).domain⊢ ↑(unitaryConj u A + I • 1) ⟨x, hf⟩ = ↑(unitaryConj u A - -I • 1) ⟨x, hg⟩refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A + I • 1).toFun.range = ⊤ simp [sub_apply, add_apply, smul_apply, sub_neg_eq_add]refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A + I • 1).toFun.range = ⊤refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A + I • 1).toFun.range = ⊤
    rw [hIrefine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A - -I • 1).toFun.range = ⊤refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A - -I • 1).toFun.range = ⊤]refine_1H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (unitaryConj u A - -I • 1).toFun.range = ⊤
    exact hrange (byH:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤hI:unitaryConj u A + I • 1 = unitaryConj u A - -I • 1⊢ (-I).im ≠ 0 norm_numAll goals completed! 🐙)
  ·refine_2H:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ (unitaryConj u A - I • 1).toFun.range = ⊤ exact hrange (byH:Type u_1H':Type u_2inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ Hinst✝³:CompleteSpace Hinst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] HhA:IsSelfAdjoint Ahrange:∀ {z : ℂ}, z.im ≠ 0 → (unitaryConj u A - z • 1).toFun.range = ⊤⊢ I.im ≠ 0 norm_numAll goals completed! 🐙)