Hilbert space direct sums and componentwise self-adjoint operators #
The blueprint's external Hilbert space direct sum ⨁ⱼ Hⱼ is Mathlib's lp G 2, and the
internal notion — a family of pairwise orthogonal closed subspaces of H summing to H
— is recorded here as IsInternalOrthogonalDecomposition, identified with the external
one through Mathlib's IsHilbertSum.
The payoff is the pair of propositions saying that an operator acting componentwise by a family of bounded self-adjoint operators, defined at least on the finite direct sum, is essentially self-adjoint with closure given by the same componentwise formula on the maximal domain.
Main definitions #
Physicslib4.Spectral.Unbounded.IsInternalOrthogonalDecompositionPhysicslib4.Spectral.Unbounded.IsDirectSumOperator,Physicslib4.Spectral.Unbounded.directSumDomain(external form)Physicslib4.Spectral.Unbounded.IsInternalDirectSumOperator,Physicslib4.Spectral.Unbounded.internalDomain(internal form)
Main statements #
dense_setOf_finite_support— the finite direct sum is dense.isHilbertSum_of_isInternalOrthogonalDecomposition— an internal decomposition is unitarily the external direct sum of its summands.isEssentiallySelfAdjoint_of_isDirectSumOperatorand companions — the external form of the blueprint's Proposition 9.26.isEssentiallySelfAdjoint_of_isInternalDirectSumOperatorand companions — its internal form.
The external Hilbert space direct sum #
The blueprint's ⨁ⱼ Hⱼ — square-summable sequences with the componentwise inner product
— is Mathlib's lp G 2 together with lp.instInnerProductSpace.
The finite direct sum — the elements of ⨁ᵢ Gᵢ with only finitely many non-zero entries
— is dense. (That it is a subspace is immediate, a linear combination of two
finitely-supported families again being finitely supported.)
Blueprint reference: lmm:finite-direct-sum-dense.
Internal orthogonal decompositions #
A sequence K(0), K(1), … of closed subspaces splits H as an orthogonal direct sum: the subspaces are pairwise orthogonal and every vector is a norm-convergent series ψ = Σ ψₙ with ψₙ in K(n).
This is how a Hilbert space is split into sectors inside itself, for example into the
eigenspaces of a Hamiltonian with discrete spectrum, or into the n-particle subspaces of a Fock
space. The decomposition ψ = Σ ψₙ is unique, ‖ψ‖² = Σ ‖ψₙ‖², and the map ψ ↦ (ψ₀, ψ₁, …)
identifies H with the external direct sum of the K(n)
(isHilbertSum_of_isInternalOrthogonalDecomposition).
Implementation note: the summands are indexed by ℕ, as in the blueprint, and are
Submodule ℂ Hs. Mathlib's notion for the same situation is IsHilbertSum for the inclusions
of the summands; this structure states the blueprint's definition directly, and
isHilbertSum_of_isInternalOrthogonalDecomposition converts it.
Blueprint: def:internal-orthogonal-decomposition
Each subspace K(n) is closed in H.
Vectors of different subspaces K(n) and K(m), n ≠ m, are orthogonal.
Every ψ in H is the sum of a norm-convergent series Σ ψₙ with ψₙ in K(n).
Instances For
The decomposition of a vector along an internal orthogonal decomposition is unique.
Blueprint reference: lmm:internal-decomposition-unitary (Part 1).
Pythagoras for an internal orthogonal decomposition: ‖ψ‖² = ∑ₙ ‖ψₙ‖².
Blueprint reference: lmm:internal-decomposition-unitary (Part 2).
An internal orthogonal decomposition of H identifies H with the external direct sum of its subspaces, by a unitary map.
The map sends ψ to the sequence (ψ₀, ψ₁, …) of its components, which is square-summable because ‖ψ‖² = Σ ‖ψₙ‖². It is linear, bijective and preserves inner products, so H and the external direct sum of the K(n) are the same Hilbert space for every purpose of quantum mechanics.
Implementation note: the conclusion is Mathlib's IsHilbertSum for the inclusions
(K n).subtypeₗᵢ; the unitary map is then IsHilbertSum.linearIsometryEquiv.
Blueprint: lmm:internal-decomposition-unitary (Part 3)
Componentwise self-adjoint operators, external form #
The domain V of the operator acting componentwise by a family of bounded operators Aᵢ on an external direct sum: the vectors ψ = (ψᵢ) with Σ (‖ψᵢ‖² + ‖Aᵢψᵢ‖²) finite.
If each Aᵢ is bounded but their norms are not uniformly bounded, the sequence (Aᵢψᵢ) need not be
square-summable, so the componentwise operator ψ ↦ (Aᵢψᵢ) is unbounded and V is the largest
domain on which it makes sense. A Hamiltonian that is block-diagonal with respect to a
decomposition into sectors, with energies growing from sector to sector, is of this kind.
For self-adjoint Aᵢ, V is the domain of the closure and of the adjoint of any
IsDirectSumOperator for the family (domain_closure_eq_directSumDomain,
domain_adjoint_eq_directSumDomain).
Implementation note: the external direct sum of the Hilbert spaces G(i) is Mathlib's
lp G 2, and V is a set of its elements. The index type is arbitrary, not only ℕ.
Blueprint: prpstn:hall-9.26
Equations
Instances For
An operator T on an external direct sum acts componentwise by a family of bounded operators Aᵢ: T is symmetric, its domain contains every vector with finitely many nonzero components, and on such vectors (Tψ)ᵢ = Aᵢψᵢ.
This fixes T only on the finite direct sum, a dense subspace; T may be defined on more. When
every Aᵢ is self-adjoint, T is essentially self-adjoint, and its closure and its adjoint are the
same operator ψ ↦ (Aᵢψᵢ) on the domain V of directSumDomain
(isEssentiallySelfAdjoint_of_isDirectSumOperator, closure_apply_eq_of_isDirectSumOperator,
adjoint_apply_eq_of_isDirectSumOperator). So the componentwise operator has exactly one
self-adjoint version, whichever dense domain it is first written on.
Implementation note: the structure is a predicate on a given partial linear map T on
lp G 2, rather than a construction of T, matching the blueprint's "suppose A is a symmetric
operator ...".
Blueprint: prpstn:hall-9.26
- isSymmetric : IsSymmetric T
The operator T is symmetric.
Every vector with finitely many nonzero components lies in the domain of T.
On a vector ψ with finitely many nonzero components, (Tψ)ᵢ = Aᵢψᵢ for every i.
Instances For
An operator acting componentwise by bounded self-adjoint operators on an external direct sum is essentially self-adjoint.
Each Aᵢ ∓ i𝟙 is surjective on its summand, because the spectrum of a bounded self-adjoint
operator is real; so the ranges of T ∓ i𝟙 contain the dense finite direct sum, and the basic
criterion for essential self-adjointness applies (isEssentiallySelfAdjoint_iff_dense_range).
Blueprint: prpstn:hall-9.26
The domain of the closure is the maximal domain V.
Blueprint reference: prpstn:hall-9.26.
The domain of the adjoint is the maximal domain V.
Blueprint reference: prpstn:hall-9.26.
On V, the closure acts componentwise by A.
Blueprint reference: prpstn:hall-9.26.
On V, the adjoint acts componentwise by A.
Blueprint reference: prpstn:hall-9.26.
Componentwise self-adjoint operators, internal form #
The domain V of the operator acting by bounded operators Aₙ on the subspaces K(n) of H: the vectors ψ = Σ ψₙ, with ψₙ in K(n), for which Σ (‖ψₙ‖² + ‖Aₙψₙ‖²) is finite.
This is directSumDomain transported to a decomposition of H into subspaces. For an internal
orthogonal decomposition K and self-adjoint Aₙ, V is the domain of the closure and of the
adjoint of any IsInternalDirectSumOperator for the family (domain_closure_eq_internalDomain,
domain_adjoint_eq_internalDomain).
Implementation note: the definition asks for some series Σ ψₙ converging to ψ with the
summability condition; for an internal orthogonal decomposition that series is unique
(hasSum_injective_of_isInternalOrthogonalDecomposition).
Blueprint: prpstn:hall-9.26-internal
Equations
Instances For
An operator T on H acts by bounded operators Aₙ on the subspaces K(n): T is symmetric, its domain contains every finite sum η₀ + … + η(N−1) with ηₙ in K(n), and T sends that sum to A₀η₀ + … + A(N−1)η(N−1).
This is IsDirectSumOperator for a decomposition of H into subspaces, the form in which the
blueprint applies it. For an internal orthogonal decomposition K and self-adjoint Aₙ, T is
essentially self-adjoint, and its closure and its adjoint both send ψ = Σ ψₙ in
internalDomain to Σ Aₙψₙ (isEssentiallySelfAdjoint_of_isInternalDirectSumOperator,
hasSum_closure_apply_of_isInternalDirectSumOperator,
hasSum_adjoint_apply_of_isInternalDirectSumOperator).
Implementation note: the finite sums are written as sums over Finset.range N of an arbitrary
family η with η n in K(n); these are exactly the vectors of the algebraic span of the K(n).
Blueprint: prpstn:hall-9.26-internal
- isSymmetric : IsSymmetric T
The operator T is symmetric.
Every finite sum η₀ + … + η(N−1) with ηₙ in K(n) lies in the domain of T.
- apply_eq (N : ℕ) (η : (n : ℕ) → ↥(K n)) : ↑T ⟨∑ n ∈ Finset.range N, ↑(η n), ⋯⟩ = ∑ n ∈ Finset.range N, ↑((A n) (η n))
T sends η₀ + … + η(N−1) to A₀η₀ + … + A(N−1)η(N−1).
Instances For
An operator acting by bounded self-adjoint operators on the subspaces of an internal orthogonal decomposition is essentially self-adjoint.
This is the internal form of isEssentiallySelfAdjoint_of_isDirectSumOperator, with the same
proof: each subspace K(n) lies in the ranges of T ∓ i𝟙, and the K(n) together span a dense
subspace of H.
Implementation note: the instance [∀ n, CompleteSpace (K n)] (needed for
IsSelfAdjoint (A n), which uses the Hilbert adjoint on K n →L[ℂ] K n) is not a restriction:
it follows from hK.isClosed via IsClosed.completeSpace_coe, so a caller can always supply
it with haveI.
Blueprint: prpstn:hall-9.26-internal
The domain of the closure is the maximal internal domain.
Remark: the instance [∀ n, CompleteSpace (K n)] (needed for IsSelfAdjoint (A n), which
uses the Hilbert adjoint on K n →L[ℂ] K n) is not a restriction: it follows from hK.isClosed
via IsClosed.completeSpace_coe, so a caller can always supply it with haveI.
Blueprint reference: prpstn:hall-9.26-internal.
The domain of the adjoint is the maximal internal domain.
Remark: the instance [∀ n, CompleteSpace (K n)] (needed for IsSelfAdjoint (A n), which
uses the Hilbert adjoint on K n →L[ℂ] K n) is not a restriction: it follows from hK.isClosed
via IsClosed.completeSpace_coe, so a caller can always supply it with haveI.
Blueprint reference: prpstn:hall-9.26-internal.
On the maximal internal domain, the closure is given by the norm-convergent sum
∑ₙ Aₙ ψₙ.
Remark: the instance [∀ n, CompleteSpace (K n)] (needed for IsSelfAdjoint (A n), which
uses the Hilbert adjoint on K n →L[ℂ] K n) is not a restriction: it follows from hK.isClosed
via IsClosed.completeSpace_coe, so a caller can always supply it with haveI.
Blueprint reference: prpstn:hall-9.26-internal.
The same formula for the adjoint.
Remark: the instance [∀ n, CompleteSpace (K n)] (needed for IsSelfAdjoint (A n), which
uses the Hilbert adjoint on K n →L[ℂ] K n) is not a restriction: it follows from hK.isClosed
via IsClosed.completeSpace_coe, so a caller can always supply it with haveI.
Blueprint reference: prpstn:hall-9.26-internal.