Physicslib4.Spectral.Unbounded.Basic

Unbounded operators: adjoint, symmetry, self-adjointness and closure

This file formalizes the first part of the blueprint section on unbounded spectral theorems: the basic theory of an unbounded operator on a separable complex Hilbert space H.

The blueprint's unbounded operator A : Dom(A) → H, with Dom(A) a dense subspace of H, is Mathlib's partially defined linear map T : H →ₗ.[ℂ] H together with the hypothesis HasDenseDomain T. Its adjoint is Mathlib's LinearPMap.adjoint (notation T†), "A is an extension of B" is B ≤ T, and closedness/closability/closure are Mathlib's LinearPMap.IsClosed, LinearPMap.IsClosable and LinearPMap.closure. Self-adjointness is _root_.IsSelfAdjoint for the Star instance on H →ₗ.[ℂ] H, which is T† = T.

Main definitions

• Physicslib4.Spectral.Unbounded.HasDenseDomain — the blueprint's standing hypothesis on an unbounded operator.
• Physicslib4.Spectral.Unbounded.IsSymmetric — ⟪φ, T ψ⟫ = ⟪T φ, ψ⟫ on Dom(T).
• Physicslib4.Spectral.Unbounded.IsEssentiallySelfAdjoint — symmetric, closable, with self-adjoint closure.
• Physicslib4.Spectral.Unbounded.ker, Physicslib4.Spectral.Unbounded.range — kernel and range of an unbounded operator, as subspaces of H.
• Physicslib4.Spectral.Unbounded.subSmul — the operator T - λ 1 with domain Dom(T).

Main statements

• existsUnique_adjoint_apply — the adjoint is well defined.
• mem_adjoint_domain_iff_exists, adjoint_apply_eq_of_forall_inner — membership in Dom(T*) via an exact representation.
• isSymmetric_iff_le_adjoint — T is symmetric iff T* extends T.
• mem_domain_closure_iff, closure_apply_eq_of_tendsto, closure_le_of_isClosed — the sequential description of the closure, and its minimality.
• isClosable_of_isSymmetric, adjoint_closure_eq_adjoint, adjoint_le_adjoint_of_le, existsUnique_isSelfAdjoint_extension, eq_closure_of_isSelfAdjoint_of_le.
• orthogonal_range_eq_ker_adjoint — Range(T)ᗮ = Ker(T*).
• adjoint_add_toPMap, isSelfAdjoint_add_of_isSelfAdjoint — adjoint of a sum with a bounded operator.
• isClosed_range_subSmul — a uniform lower bound forces Range(T - λ 1) to be closed.

def Physicslib4.Spectral.Unbounded.HasDenseDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Prop

The domain of a partially defined linear map T on H is dense: the condition that makes T an unbounded operator.

Position, momentum and most Hamiltonians of quantum mechanics cannot be defined on every vector of H, only on a subspace of it. An unbounded operator is therefore a pair: a subspace Dom(T) of H, its domain, and a linear map T : Dom(T) → H, with Dom(T) dense in H. "Unbounded" means "not necessarily bounded": a bounded operator defined on all of H is a special case. Density of Dom(T) is what makes the adjoint T* well defined (existsUnique_adjoint_apply).

Implementation note: the pair (Dom(T), T) is Mathlib's LinearPMap, written H →ₗ.[ℂ] H, with domain T.domain. Density is not part of the type: it is this predicate, carried as an explicit hypothesis wherever the blueprint requires a dense domain. A self-adjoint operator has dense domain automatically (Mathlib's IsSelfAdjoint.dense_domain).

Blueprint: def:hall-3.1

Equations

• Physicslib4.Spectral.Unbounded.HasDenseDomain T = Dense ↑T.domain

The adjoint

The blueprint's Dom(A*) is the set of φ for which ψ ↦ ⟪φ, A ψ⟫ is bounded on Dom(A); this is Mathlib's LinearPMap.adjointDomain, phrased there as continuity of that functional, and A* itself is LinearPMap.adjoint, written T†.

theorem Physicslib4.Spectral.Unbounded.existsUnique_adjoint_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) {φ : H} (hφ : φ ∈ T.adjoint.domain) : ∃! χ : H, ∀ (ψ : ↥T.domain), inner ℂ φ (↑T ψ) = inner ℂ χ ↑ψ

The adjoint of a densely defined operator is well defined: for φ in Dom(T*) exactly one vector χ satisfies ⟨φ, Tψ⟩ = ⟨χ, ψ⟩ for all ψ in Dom(T).

The adjoint T* is defined on the vectors φ for which ψ ↦ ⟨φ, Tψ⟩ is bounded on Dom(T); the Riesz representation theorem then gives a vector χ with ⟨φ, Tψ⟩ = ⟨χ, ψ⟩, and T*φ = χ. That χ is unique because a vector orthogonal to the dense subspace Dom(T) is 0. For a bounded operator on all of H this is the usual Hermitian conjugate A†.

Implementation note: the adjoint is Mathlib's LinearPMap.adjoint, written T†, with domain LinearPMap.adjointDomain (continuity of ψ ↦ ⟨φ, Tψ⟩, which is boundedness). When T.domain is not dense, Mathlib's T† keeps the domain adjointDomain but is the zero map there; this is why the density hypothesis is needed here.

Blueprint: prpstn:adjoint-well-defined

theorem Physicslib4.Spectral.Unbounded.smul_add_mem_adjoint_domain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (α β : ℂ) {φ₁ φ₂ : H} (h₁ : φ₁ ∈ T.adjoint.domain) (h₂ : φ₂ ∈ T.adjoint.domain) : α • φ₁ + β • φ₂ ∈ T.adjoint.domain

A linear combination of vectors in Dom(T*) again lies in Dom(T*).

Together with adjoint_smul_add this is the blueprint's linearity of the adjoint; in Lean it is already carried by the fact that T† is a LinearPMap, whose domain is a submodule and whose action is linear.

Blueprint reference: prpstn:hall-linearity-of-the-adjoint.

theorem Physicslib4.Spectral.Unbounded.adjoint_smul_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (α β : ℂ) (φ₁ φ₂ : ↥T.adjoint.domain) (h : α • ↑φ₁ + β • ↑φ₂ ∈ T.adjoint.domain) : ↑T.adjoint ⟨α • ↑φ₁ + β • ↑φ₂, h⟩ = α • ↑T.adjoint φ₁ + β • ↑T.adjoint φ₂

The adjoint acts linearly on its domain.

Blueprint reference: prpstn:hall-linearity-of-the-adjoint.

theorem Physicslib4.Spectral.Unbounded.mem_adjoint_domain_iff_exists {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (ψ : H) : ψ ∈ T.adjoint.domain ↔ ∃ (φ : H), ∀ (χ : ↥T.domain), inner ℂ ψ (↑T χ) = inner ℂ φ ↑χ

A vector ψ lies in Dom(T*) exactly when the functional χ ↦ ⟪ψ, T χ⟫ is exactly represented by some vector φ; boundedness need not be checked directly.

Blueprint reference: lmm:characterizing-adjoint-domain-membership.

theorem Physicslib4.Spectral.Unbounded.adjoint_apply_eq_of_forall_inner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) {ψ : H} (hψ : ψ ∈ T.adjoint.domain) {φ : H} (h : ∀ (χ : ↥T.domain), inner ℂ ψ (↑T χ) = inner ℂ φ ↑χ) : ↑T.adjoint ⟨ψ, hψ⟩ = φ

The representing vector in mem_adjoint_domain_iff_exists is T* ψ.

Blueprint reference: lmm:characterizing-adjoint-domain-membership.

Symmetric, self-adjoint and essentially self-adjoint operators

def Physicslib4.Spectral.Unbounded.IsSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Prop

An operator T is symmetric if ⟨φ, Tψ⟩ = ⟨Tφ, ψ⟩ for all φ and ψ in its domain.

This is the condition physicists usually call "Hermitian": it makes every expectation value ⟨ψ, Tψ⟩ real. For an unbounded operator it is weaker than self-adjointness. A densely defined T is symmetric exactly when T* extends T (isSymmetric_iff_le_adjoint), while self-adjointness asks T* = T, including equal domains. The reality of the spectrum (pmapSpectrum_subset_real) and the spectral theorem need self-adjointness, so the gap between the two notions matters.

Implementation note: no density of T.domain is assumed; the blueprint's operators have dense domain, supplied separately by HasDenseDomain. The predicate is Mathlib's LinearPMap.IsFormalAdjoint of T with itself, with the sides of the equation swapped (isSymmetric_iff_isFormalAdjoint). Self-adjointness is Mathlib's IsSelfAdjoint for the star operation T ↦ T† on H →ₗ.[ℂ] H, so it means T† = T (LinearPMap.isSelfAdjoint_def).

Blueprint: def:hall-9.2

Equations

• Physicslib4.Spectral.Unbounded.IsSymmetric T = ∀ (φ ψ : ↥T.domain), inner ℂ (↑φ) (↑T ψ) = inner ℂ (↑T φ) ↑ψ

theorem Physicslib4.Spectral.Unbounded.isSymmetric_iff_isFormalAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} : IsSymmetric T ↔ T.IsFormalAdjoint T

Symmetry in the sense of IsSymmetric is Mathlib's LinearPMap.IsFormalAdjoint of T with itself.

Blueprint reference: def:hall-9.2.

theorem Physicslib4.Spectral.Unbounded.isSymmetric_iff_le_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) : IsSymmetric T ↔ T ≤ T.adjoint

An unbounded operator is symmetric if and only if its adjoint is an extension of it.

Blueprint reference: prpstn:hall-9.4.

def Physicslib4.Spectral.Unbounded.IsPositive {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (A : H →ₗ.[ℂ] H) : Prop

An operator A is positive if it is symmetric and ⟨ψ, Aψ⟩ ≥ 0 for every ψ in its domain.

For a symmetric A the expectation value ⟨ψ, Aψ⟩ is real, so the condition says that every expectation value is non-negative. This is the notion in which the positive-energy condition of the Haag–Kastler axioms is phrased: a one-parameter unitary group has positive energy when its generator is positive (Physicslib4.AQFT.IsPositiveEnergy). For a bounded operator on all of H it agrees with the usual positivity (isPositive_toPMap_iff).

Implementation note: the condition is stated as 0 ≤ Re⟨ψ, Aψ⟩, the form of Mathlib's ContinuousLinearMap.IsPositive. Symmetry is meant in the density-free sense of IsSymmetric.

Blueprint: def:positive-unbounded-operator

Equations

• Physicslib4.Spectral.Unbounded.IsPositive A = (Physicslib4.Spectral.Unbounded.IsSymmetric A ∧ ∀ (ψ : ↥A.domain), 0 ≤ (inner ℂ (↑ψ) (↑A ψ)).re)

theorem Physicslib4.Spectral.Unbounded.isPositive_toPMap_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (P : H →L[ℂ] H) : IsPositive ((↑P).toPMap ⊤) ↔ P.IsPositive

A bounded operator, regarded as an unbounded operator with domain H, is positive exactly when it is positive as a bounded operator.

Blueprint reference: lmm:positive-bounded-agrees.

theorem Physicslib4.Spectral.Unbounded.IsPositive.of_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {A B : H →ₗ.[ℂ] H} (hA : IsPositive A) (W : H ≃ₗᵢ[ℂ] H) (hdom : ∀ (ψ : H), ψ ∈ B.domain ↔ W.symm ψ ∈ A.domain) (happ : ∀ (ψ : H) (h : ψ ∈ B.domain) (h' : W.symm ψ ∈ A.domain), ↑B ⟨ψ, h⟩ = W (↑A ⟨W.symm ψ, h'⟩)) : IsPositive B

Unitary conjugation preserves positivity: if A is positive, W is unitary, and B has domain W · Dom(A) with B ψ = W A W⁻¹ ψ there, then B is positive. Stated through the domain and the formula rather than by building W A W⁻¹, which is the form in which Stone.mem_generator_conj_domain_iff and Stone.generator_conj_apply supply it.

Blueprint reference: lmm:positive-conj.

The closure of an unbounded operator

The blueprint's graph Γ(A) ⊂ H × H is Mathlib's LinearPMap.graph, closedness and closability are LinearPMap.IsClosed and LinearPMap.IsClosable, and A^cl is LinearPMap.closure.

theorem Physicslib4.Spectral.Unbounded.isClosed_iff_forall_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} : T.IsClosed ↔ ∀ (χ : ℕ → ↥T.domain) (ψ φ : H), Filter.Tendsto (fun (n : ℕ) => ↑(χ n)) Filter.atTop (nhds ψ) → Filter.Tendsto (fun (n : ℕ) => ↑T (χ n)) Filter.atTop (nhds φ) → ∃ (hψ : ψ ∈ T.domain), ↑T ⟨ψ, hψ⟩ = φ

An operator T is closed exactly when ψ_n → ψ and Tψ_n → φ, with every ψ_n in Dom(T), imply that ψ lies in Dom(T) and Tψ = φ.

Closedness is the regularity condition that replaces continuity for unbounded operators. An operator that is not bounded is not continuous on its domain, but if T is closed then, whenever ψ_n → ψ and Tψ_n converges at all, the limit is Tψ. By definition T is closed when its graph {(ψ, Tψ) : ψ ∈ Dom(T)} is a closed subset of H × H; this theorem restates that with sequences. The adjoint of a densely defined operator is closed, so every self-adjoint operator is closed. A closable operator T, one whose graph has a closure that is again a graph, has a smallest closed extension, its closure T^(cl) (closure_le_of_isClosed).

Implementation note: closedness, closability and closure are Mathlib's LinearPMap.IsClosed, LinearPMap.IsClosable and LinearPMap.closure, with the graph LinearPMap.graph. No density of T.domain is assumed, so the statement applies to adjoints, whose domains need not be dense.

Blueprint: def:closed-linear-map-on-a-subspace

theorem Physicslib4.Spectral.Unbounded.hasDenseDomain_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (_hc : T.IsClosable) : HasDenseDomain T.closure

The closure of a densely defined closable operator again has dense domain, so it is again an unbounded operator in the blueprint's sense.

Blueprint reference: prpstn:closure-linearity-and-sequential-description (Part 1).

theorem Physicslib4.Spectral.Unbounded.mem_domain_closure_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hc : T.IsClosable) (ξ : H) : ξ ∈ T.closure.domain ↔ ∃ (χ : ℕ → ↥T.domain) (η : H), Filter.Tendsto (fun (n : ℕ) => ↑(χ n)) Filter.atTop (nhds ξ) ∧ Filter.Tendsto (fun (n : ℕ) => ↑T (χ n)) Filter.atTop (nhds η)

Sequential description of the domain of the closure: ξ ∈ Dom(T^cl) exactly when there is a sequence in Dom(T) converging to ξ whose image under T also converges.

Blueprint reference: prpstn:closure-linearity-and-sequential-description (Part 2).

theorem Physicslib4.Spectral.Unbounded.closure_apply_eq_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hc : T.IsClosable) {ξ η : H} {χ : ℕ → ↥T.domain} (hχ : Filter.Tendsto (fun (n : ℕ) => ↑(χ n)) Filter.atTop (nhds ξ)) (hTχ : Filter.Tendsto (fun (n : ℕ) => ↑T (χ n)) Filter.atTop (nhds η)) (hξ : ξ ∈ T.closure.domain) : ↑T.closure ⟨ξ, hξ⟩ = η

In the situation of mem_domain_closure_iff, the limit of T χ n is T^cl ξ.

Blueprint reference: prpstn:closure-linearity-and-sequential-description (Part 2).

theorem Physicslib4.Spectral.Unbounded.closure_le_of_isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T B : H →ₗ.[ℂ] H} (hc : T.IsClosable) (hTB : T ≤ B) (hB : B.IsClosed) : T.closure ≤ B

T^cl is the smallest closed extension of T: any closed extension of T is an extension of T^cl. (That T^cl is itself a closed extension of T is Mathlib's LinearPMap.le_closure and LinearPMap.IsClosable.closure_isClosed.)

Blueprint reference: prpstn:closure-linearity-and-sequential-description (Part 3).

theorem Physicslib4.Spectral.Unbounded.isSymmetric_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} (hsym : IsSymmetric T) (hc : T.IsClosable) : IsSymmetric T.closure

The closure of a symmetric closable operator is symmetric.

Blueprint reference: lmm:closure-of-symmetric-is-symmetric.

structure Physicslib4.Spectral.Unbounded.IsEssentiallySelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →ₗ.[ℂ] H) : Prop

An operator T is essentially self-adjoint if it is symmetric and closable, and its closure is self-adjoint.

In practice an observable is often first written down on a convenient small domain, for example the momentum operator −i d/dx on smooth compactly supported wave functions. There it is symmetric but not self-adjoint. Essential self-adjointness says that the domain is nevertheless big enough: the closure T^(cl) is self-adjoint, and it is the only self-adjoint extension of T (existsUnique_isSelfAdjoint_extension). A densely defined symmetric T is essentially self-adjoint exactly when T − i𝟙 and T + i𝟙 have dense ranges (isEssentiallySelfAdjoint_iff_dense_range).

Implementation note: the closure is Mathlib's LinearPMap.closure, and self-adjointness is T.closure† = T.closure. The three conditions are kept as separate fields, as in the blueprint, although closability follows from symmetry for densely defined T (isClosable_of_isSymmetric).

Blueprint: def:hall-9.7

• isSymmetric : IsSymmetric T

  T is symmetric: ⟨φ, Tψ⟩ = ⟨Tφ, ψ⟩ on Dom(T).

• isClosable : T.IsClosable

  T is closable: the closure of its graph in H × H is the graph of an operator.

• isSelfAdjoint_closure : IsSelfAdjoint T.closure

  The closure T^(cl) of T is self-adjoint.

Elementary properties of adjoints and closed operators

theorem Physicslib4.Spectral.Unbounded.isClosable_of_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (hsym : IsSymmetric T) : T.IsClosable

A symmetric operator is always closable.

(Part 1 of the blueprint statement — that the graph of T* is closed, with no hypothesis on T beyond dense domain — is Mathlib's LinearPMap.adjoint_isClosed.)

Blueprint reference: prpstn:hall-9.8 (Part 2).

theorem Physicslib4.Spectral.Unbounded.adjoint_closure_eq_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (hc : T.IsClosable) : T.closure.adjoint = T.adjoint

The adjoint of the closure of a closable operator coincides with the adjoint of the operator itself.

Blueprint reference: prpstn:hall-9.10.

theorem Physicslib4.Spectral.Unbounded.adjoint_le_adjoint_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {C₁ C₂ : H →ₗ.[ℂ] H} (hC₂ : HasDenseDomain C₂) (h : C₂ ≤ C₁) : C₁.adjoint ≤ C₂.adjoint

Taking adjoints reverses extension: if C₁ extends C₂ then C₂* extends C₁*, i.e. Dom(C₁*) ⊆ Dom(C₂*) and C₁*, C₂* agree on Dom(C₁*).

The density hypothesis on Dom(C₂) (which forces density of Dom(C₁) ⊇ Dom(C₂)) is the blueprint's standing assumption that both are unbounded operators. It cannot be dropped: Mathlib's LinearPMap.adjoint is the zero map on its domain when the domain of the operator is not dense, so for C₂ with non-dense domain and C₁ densely defined the conclusion would say that C₁† is the zero map on its domain.

Blueprint reference: lmm:extension-reverses-adjoint-domains.

theorem Physicslib4.Spectral.Unbounded.eq_of_isSelfAdjoint_of_isSymmetric_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A B : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (hB : IsSymmetric B) (hAB : A ≤ B) : A = B

A self-adjoint operator has no proper symmetric extension: if B is symmetric and extends the self-adjoint A, then A = B.

B need not be assumed densely defined: its domain contains the dense domain of A.

Blueprint reference: lmm:self-adjoint-maximally-symmetric.

theorem Physicslib4.Spectral.Unbounded.eq_closure_of_isSelfAdjoint_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T B : H →ₗ.[ℂ] H} (h : IsEssentiallySelfAdjoint T) (hB : IsSelfAdjoint B) (hTB : T ≤ B) : B = T.closure

Every self-adjoint extension of an essentially self-adjoint operator T is T^cl.

Blueprint reference: prpstn:hall-9.11.

theorem Physicslib4.Spectral.Unbounded.existsUnique_isSelfAdjoint_extension {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (h : IsEssentiallySelfAdjoint T) : ∃! B : H →ₗ.[ℂ] H, IsSelfAdjoint B ∧ T ≤ B

If T is essentially self-adjoint, then T^cl is the unique self-adjoint extension of T. The identification of the witness is eq_closure_of_isSelfAdjoint_of_le.

Blueprint reference: prpstn:hall-9.11.

Orthogonal complements and density

Part 2 of prpstn:hall-a.49, (Vᗮ)ᗮ = closure V, is Mathlib's Submodule.orthogonal_orthogonal_eq_closure.

theorem Physicslib4.Spectral.Unbounded.existsUnique_add_mem_orthogonal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {V : Submodule ℂ H} (hV : IsClosed ↑V) (ψ : H) : ∃! p : H × H, p.1 ∈ V ∧ p.2 ∈ Vᗮ ∧ ψ = p.1 + p.2

Orthogonal decomposition: if V is a closed subspace of H, every ψ decomposes uniquely as ψ = ψ₁ + ψ₂ with ψ₁ ∈ V and ψ₂ ∈ Vᗮ.

Blueprint reference: prpstn:hall-a.49 (Part 1).

theorem Physicslib4.Spectral.Unbounded.dense_iff_orthogonal_eq_bot {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {V : Submodule ℂ H} : Dense ↑V ↔ Vᗮ = ⊥

A subspace V of H is dense if and only if Vᗮ = {0}.

Blueprint reference: crllr:trivial-complement-characterizes-density.

theorem Physicslib4.Spectral.Unbounded.adjoint_smul_id {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (lam : ℂ) : ContinuousLinearMap.adjoint (lam • ContinuousLinearMap.id ℂ H) = (starRingEnd ℂ) lam • ContinuousLinearMap.id ℂ H

The adjoint of the bounded operator λ 1 is λ̄ 1.

Blueprint reference: lmm:adjoint-of-scalar-multiple-of-identity.

Kernel and range

def Physicslib4.Spectral.Unbounded.ker {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Submodule ℂ H

The kernel Ker(T) = {ψ ∈ Dom(T) : Tψ = 0} of an operator T, as a subspace of H.

The restriction to Dom(T) is part of the definition: a vector outside Dom(T) is never in Ker(T). The kernel of T − λ𝟙 is the eigenspace of T for the eigenvalue λ, and Range(T)ᗮ = Ker(T*) (orthogonal_range_eq_ker_adjoint) turns questions about the range of T into questions about the kernel of T*.

Implementation note: the kernel of the linear map T.toFun : T.domain →ₗ[ℂ] H lives in the subtype T.domain; this definition maps it into H. Membership is mem_ker.

Blueprint: def:kernel-of-an-unbounded-operator

Equations

• Physicslib4.Spectral.Unbounded.ker T = Submodule.map T.domain.subtype T.toFun.ker

@[simp]

theorem Physicslib4.Spectral.Unbounded.mem_ker {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} {ψ : H} : ψ ∈ ker T ↔ ∃ (h : ψ ∈ T.domain), ↑T ⟨ψ, h⟩ = 0

def Physicslib4.Spectral.Unbounded.range {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) : Submodule ℂ H

The range Range(T) = {Tψ : ψ ∈ Dom(T)} of an operator T, as a subspace of H.

Its orthogonal complement consists of the vectors orthogonal to Tψ for every ψ in Dom(T) (not every ψ in H), and it equals Ker(T*) (orthogonal_range_eq_ker_adjoint). Density of the ranges of T − i𝟙 and T + i𝟙 characterises essential self-adjointness (isEssentiallySelfAdjoint_iff_dense_range).

Implementation note: the range of the linear map T.toFun : T.domain →ₗ[ℂ] H, which already lies in H. Membership is mem_range, which holds by definition.

Blueprint: def:range-of-an-unbounded-operator

Equations

• Physicslib4.Spectral.Unbounded.range T = T.toFun.range

@[simp]

theorem Physicslib4.Spectral.Unbounded.mem_range {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : H →ₗ.[ℂ] H} {φ : H} : φ ∈ range T ↔ ∃ (ψ : ↥T.domain), ↑T ψ = φ

theorem Physicslib4.Spectral.Unbounded.orthogonal_range_eq_ker_adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) : (range T)ᗮ = ker T.adjoint

The orthogonal complement of the range of T is the kernel of T*.

Blueprint reference: prpstn:hall-9.12.

Sums with a bounded operator, and T - λ 1

theorem Physicslib4.Spectral.Unbounded.adjoint_add_toPMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (B : H →L[ℂ] H) : (T + (↑B).toPMap ⊤).adjoint = T.adjoint + (↑(ContinuousLinearMap.adjoint B)).toPMap ⊤

The adjoint of T + B, for B a bounded operator defined on all of H, has the same domain as T* and acts as T* + B* there. (The right-hand side has domain Dom(T*) ⊓ ⊤; the equality includes the equality of domains.)

Blueprint reference: prpstn:hall-9.13.

theorem Physicslib4.Spectral.Unbounded.isSelfAdjoint_add_of_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hTsa : IsSelfAdjoint T) {B : H →L[ℂ] H} (hB : IsSelfAdjoint B) : IsSelfAdjoint (T + (↑B).toPMap ⊤)

The sum of an unbounded self-adjoint operator and a bounded self-adjoint operator defined on all of H is self-adjoint on the domain of the unbounded one.

Blueprint reference: prpstn:hall-9.13.

def Physicslib4.Spectral.Unbounded.subSmul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (lam : ℂ) : H →ₗ.[ℂ] H

The operator T − λ𝟙 for a complex number λ, with domain Dom(T) and action ψ ↦ Tψ − λψ.

Since λ𝟙 is defined on all of H, the difference is defined exactly where T is. The resolvent set and spectrum of T are defined through the invertibility of T − λ𝟙 (IsResolvent), and the ranges of T − i𝟙 and T + i𝟙 decide essential self-adjointness.

Implementation note: T + i𝟙 is subSmul T (-Complex.I). The parameter is named lam because λ is reserved in Lean. Domain and action are subSmul_domain and subSmul_apply, both by definition.

Blueprint: def:hall-3.1

Equations

• Physicslib4.Spectral.Unbounded.subSmul T lam = { domain := T.domain, toFun := T.toFun - lam • T.domain.subtype }

@[simp]

theorem Physicslib4.Spectral.Unbounded.subSmul_domain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (lam : ℂ) : (subSmul T lam).domain = T.domain

@[simp]

theorem Physicslib4.Spectral.Unbounded.subSmul_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →ₗ.[ℂ] H) (lam : ℂ) (ψ : ↥(subSmul T lam).domain) : ↑(subSmul T lam) ψ = ↑T ψ - lam • ↑ψ

theorem Physicslib4.Spectral.Unbounded.isClosed_range_subSmul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hcl : T.IsClosed) (lam : ℂ) {ε : ℝ} (hε : 0 < ε) (hbound : ∀ (ψ : ↥T.domain), ε * ‖↑ψ‖ ≤ ‖↑T ψ - lam • ↑ψ‖) : IsClosed ↑(range (subSmul T lam))

If T is closed and ‖(T - λ 1) ψ‖ is bounded below by ε ‖ψ‖ for some ε > 0, then the range of T - λ 1 is a closed subspace of H.

Blueprint reference: prpstn:hall-9.14.

theorem Physicslib4.Spectral.Unbounded.adjoint_subSmul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (lam : ℂ) : (subSmul T lam).adjoint = subSmul T.adjoint ((starRingEnd ℂ) lam)

The adjoint of T - λ 1 is T* - λ̄ 1, including equality of domains.

Blueprint reference: prpstn:hall-9.13 with lmm:adjoint-of-scalar-multiple-of-identity.

theorem Physicslib4.Spectral.Unbounded.orthogonal_range_subSmul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (lam : ℂ) : (range (subSmul T lam))ᗮ = ker (subSmul T.adjoint ((starRingEnd ℂ) lam))

The orthogonal complement of the range of T - λ 1 is the kernel of T* - λ̄ 1.

Blueprint reference: prpstn:hall-9.12 applied to T - λ 1.