Diagonal operators on a Hilbert basis

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #93(a).

Given a Hilbert basis e : HilbertBasis ι 𝕜 E and a family of real weights l : ι → ℝ, the diagonal operator multiplies the i-th coefficient of a vector by l i. Unless the weights are bounded this takes some vectors out of the space, so it is not a ContinuousLinearMap but a LinearPMap on the natural domain of vectors whose weighted coefficients are still square-summable — the standard model of an unbounded self-adjoint operator, and the shape every operator with a known eigenbasis has.

• HilbertBasis.diagDomain e l — the natural domain, with ★ basis_mem_diagDomain (every basis vector is in it, whatever the weights) and ★★ dense_diagDomain;
• HilbertBasis.diagOp e l — the operator, with repr_diagOp its coefficients and ★ diagOp_apply_basis — each basis vector is an eigenvector with eigenvalue l i;
• ★★ diagOp_isFormalAdjoint (symmetry — the one place reality of the weights is used) and ★★★ isSelfAdjoint_diagOp — the operator is self-adjoint, the content being maximality: a vector the adjoint is defined at is already in the domain (repr_adjoint_diagOp);
• LinearPMap.IsResolventAt, LinearPMap.resolventSet and LinearPMap.spectrum — the spectrum of an operator with a domain, with ★ LinearPMap.bijective_of_isResolventAt reading the definition back (T - z is a bijection of the domain onto E) and ★ LinearPMap.mem_spectrum_of_apply_eq_smul (an eigenvalue is a spectral value);
• ★★ mem_resolventSet_diagOp and ★★ closure_range_subset_spectrum_diagOp, giving ★★★ spectrum_diagOp — the spectrum is the closure of the weight set, so a self-adjoint operator with any prescribed closed spectrum exists;
• HilbertBasis.diagCLM — the bounded companion (bounded weights, a genuine ContinuousLinearMap), which is what the resolvent is built from, plus the ℓ² multiplier lpMul and ★ Memℓp.mul_of_bddAbove underneath it.

Honest scope

⚠️ LinearPMap.spectrum is defined here, not imported. Mathlib's spectrum is defined for elements of an algebra, which an operator with a proper domain is not, so this module gives the resolvent-set definition: z is a resolvent point when T - z has a two-sided inverse that is a bounded operator on all of E. bijective_of_isResolventAt is the sanity check that this says what it should. The comparison with _root_.spectrum for a bounded operator on the domain ⊤ is not proved here; nothing below needs it.

⚠️ No functional calculus, no spectral measure, no resolution of the identity: the spectrum is computed as a set, and that is all. Nor is the standard theorem that a self-adjoint operator has real spectrum proved — for these operators it is visible in spectrum_diagOp, which exhibits the spectrum as the closure of a set of real scalars, but the general statement is a different theorem.

⚠️ The weights are real by hypothesis. A complex family gives a perfectly good operator by the same definitions, and it is symmetric only when the weights are real; nothing here is stated for the complex case.

References: the construction is the multiplication-operator model behind the spectral theorem — e.g. Reed–Simon I, Theorem VIII.4, or Rudin, Functional Analysis Ch. 13 — stated here on a Hilbert basis rather than on an L² space. Consumer: specs/BACKLOG.md #93, whose items (b) and (c) would put the twisted Laplacian of Mathlib/QuantumInfo/AharonovBohmCircle.lean into this form.

ℓ² membership at the exponent 2

theorem memℓp_two_iff {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {f : ι → 𝕜} : Memℓp f 2 ↔ Summable fun (i : ι) => ‖f i‖ ^ 2

Memℓp at the exponent 2, with the natural-number power the rest of the file uses.

theorem Memℓp.mul_of_bddAbove {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {w f : ι → 𝕜} {C : ℝ} (hw : ∀ (i : ι), ‖w i‖ ≤ C) (hf : Memℓp f 2) : Memℓp (fun (i : ι) => w i * f i) 2

★ A bounded sequence multiplies ℓ² into itself.

theorem lp.norm_mul_le_of_bddAbove {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {w : ι → 𝕜} {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) (f : ↥(lp (fun (x : ι) => 𝕜) 2)) (hwf : Memℓp (fun (i : ι) => w i * ↑f i) 2) : ‖⟨fun (i : ι) => w i * ↑f i, hwf⟩‖ ≤ C * ‖f‖

The ℓ² norm of a bounded multiple.

The bounded multiplication operator on ℓ²

noncomputable def lpMul {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) : ↥(lp (fun (x : ι) => 𝕜) 2) →L[𝕜] ↥(lp (fun (x : ι) => 𝕜) 2)

Multiplication by a bounded sequence, as a continuous linear map on ℓ².

Equations

• lpMul w hC hw = { toFun := fun (f : ↥(lp (fun (x : ι) => 𝕜) 2)) => ⟨fun (i : ι) => w i * ↑f i, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous C ⋯

@[simp]

theorem lpMul_apply {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) (f : ↥(lp (fun (x : ι) => 𝕜) 2)) (i : ι) : ↑((lpMul w hC hw) f) i = w i * ↑f i

theorem norm_lpMul_apply_le {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) (f : ↥(lp (fun (x : ι) => 𝕜) 2)) : ‖(lpMul w hC hw) f‖ ≤ C * ‖f‖

theorem memℓp_two_of_eq {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {f g : ι → 𝕜} (h : ∀ (i : ι), f i = g i) (hf : Memℓp f 2) : Memℓp g 2

Transporting ℓ² membership along a pointwise identity.

The diagonal operator of a real weight family

The resolvent set of a partially defined operator

Mathlib's spectrum is defined for elements of an algebra, which an operator with a domain is not, so the resolvent set is spelled out here: z is in it when T - z has a genuine bounded two-sided inverse.

structure LinearPMap.IsResolventAt {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (z : 𝕜) (S : E →L[𝕜] E) : Prop

S is a bounded inverse of T - z: it lands in the domain of T, it undoes T - z there, and T - z undoes it on all of E.

• maps_mem (y : E) : S y ∈ T.domain

  The inverse lands in the domain of T.

• right_inv (y : E) : ↑T ⟨S y, ⋯⟩ - z • S y = y

  T - z is a left inverse of S on all of E.

• left_inv (x : ↥T.domain) : S (↑T x - z • ↑x) = ↑x

  S is a left inverse of T - z on the domain of T.

def LinearPMap.resolventSet {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) : Set 𝕜

The resolvent set: the scalars at which T has a bounded inverse.

Equations

• T.resolventSet = {z : 𝕜 | ∃ (S : E →L[𝕜] E), T.IsResolventAt z S}

def LinearPMap.spectrum {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) : Set 𝕜

The spectrum of a partially defined operator: the complement of its resolvent set. This agrees with _root_.spectrum for a ContinuousLinearMap read as a LinearPMap on ⊤, and is stated separately because an operator with a proper domain is not an element of an algebra.

Equations

• T.spectrum = T.resolventSetᶜ

theorem LinearPMap.mem_spectrum_iff {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ.[𝕜] E} {z : 𝕜} : z ∈ T.spectrum ↔ ∀ (S : E →L[𝕜] E), ¬T.IsResolventAt z S

theorem LinearPMap.bijective_of_isResolventAt {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ.[𝕜] E} {z : 𝕜} {S : E →L[𝕜] E} (h : T.IsResolventAt z S) : Function.Bijective fun (x : ↥T.domain) => ↑T x - z • ↑x

★ At a resolvent point T - z really is a bijection of the domain onto E. This is the sanity check on the definition above: resolventSet says what the resolvent set should say.

theorem LinearPMap.mem_spectrum_of_apply_eq_smul {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ.[𝕜] E} {z : 𝕜} {x : ↥T.domain} (hx : ↑x ≠ 0) (hTx : ↑T x = z • ↑x) : z ∈ T.spectrum

★ An eigenvalue is in the spectrum.

def HilbertBasis.diagDomain {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : Submodule 𝕜 E

The natural domain of the diagonal operator with weights l: the vectors whose weighted coefficient sequence is still square-summable.

Equations

• e.diagDomain l = { carrier := {f : E | Memℓp (fun (i : ι) => ↑(l i) * ↑(e.repr f) i) 2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem HilbertBasis.mem_diagDomain_iff {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) {f : E} : f ∈ e.diagDomain l ↔ Memℓp (fun (i : ι) => ↑(l i) * ↑(e.repr f) i) 2

theorem HilbertBasis.eq_of_repr_eq {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) {x y : E} (h : ∀ (i : ι), ↑(e.repr x) i = ↑(e.repr y) i) : x = y

Two vectors with the same coefficients are equal.

theorem HilbertBasis.basis_mem_diagDomain {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) (i : ι) : e i ∈ e.diagDomain l

★ Every basis vector lies in the domain, whatever the weights.

theorem HilbertBasis.dense_diagDomain {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : Dense ↑(e.diagDomain l)

★★ The domain is dense: it contains every basis vector, and their span is dense.

noncomputable def HilbertBasis.diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : E →ₗ.[𝕜] E

The diagonal operator with weights l, as a partially defined operator on E.

Equations

• One or more equations did not get rendered due to their size.

theorem HilbertBasis.diagOp_domain {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : (e.diagOp l).domain = e.diagDomain l

@[simp]

theorem HilbertBasis.repr_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) (f : ↥(e.diagOp l).domain) (i : ι) : ↑(e.repr (↑(e.diagOp l) f)) i = ↑(l i) * ↑(e.repr ↑f) i

theorem HilbertBasis.diagOp_apply_basis {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) (i : ι) : ↑(e.diagOp l) ⟨e i, ⋯⟩ = ↑(l i) • e i

★ Every weight is an eigenvalue, with a basis vector as its eigenvector.

Symmetry and self-adjointness

theorem HilbertBasis.diagOp_isFormalAdjoint {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : (e.diagOp l).IsFormalAdjoint (e.diagOp l)

★★ The diagonal operator of a real family is symmetric. The weight comes out of either slot unchanged, which is where reality of the weights is used and the only place it is needed.

theorem HilbertBasis.repr_adjoint_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) [CompleteSpace E] (y : ↥(e.diagOp l).adjoint.domain) (i : ι) : ↑(e.repr (↑(e.diagOp l).adjoint y)) i = ↑(l i) * ↑(e.repr ↑y) i

The adjoint has the same coefficients as the operator itself: this is the computation behind maximality, and hence behind self-adjointness.

theorem HilbertBasis.isSelfAdjoint_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) [CompleteSpace E] : IsSelfAdjoint (e.diagOp l)

★★★ The diagonal operator of a real weight family is self-adjoint. Symmetry is the easy half; the content is maximality — a vector the adjoint is defined at already has a square-summable weighted coefficient sequence, so the adjoint's domain cannot be larger.

The bounded diagonal operator, and the spectrum

noncomputable def HilbertBasis.diagCLM {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) : E →L[𝕜] E

Multiplying the coefficients by a bounded family, as a continuous linear map. This is the bounded companion of diagOp, and the resolvent of diagOp is one of these.

Equations

• e.diagCLM w hC hw = e.repr.symm.toLinearIsometry.toContinuousLinearMap ∘SL lpMul w hC hw ∘SL e.repr.toLinearIsometry.toContinuousLinearMap

@[simp]

theorem HilbertBasis.repr_diagCLM {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) (y : E) (i : ι) : ↑(e.repr ((e.diagCLM w hC hw) y)) i = w i * ↑(e.repr y) i

theorem HilbertBasis.norm_diagCLM_apply_le {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (w : ι → 𝕜) {C : ℝ} (hC : 0 ≤ C) (hw : ∀ (i : ι), ‖w i‖ ≤ C) (y : E) : ‖(e.diagCLM w hC hw) y‖ ≤ C * ‖y‖

theorem HilbertBasis.mem_resolventSet_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) {z : 𝕜} (hz : z ∉ closure (Set.range fun (i : ι) => ↑(l i))) : z ∈ (e.diagOp l).resolventSet

★★ Off the closure of the weights the operator has a bounded inverse, namely the diagonal operator with the reciprocal weights. The reciprocals are bounded there — that is exactly what being off the closure says — and l i / (l i − z) is bounded too, which is what puts the inverse's values back in the domain.

theorem HilbertBasis.closure_range_subset_spectrum_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : closure (Set.range fun (i : ι) => ↑(l i)) ⊆ (e.diagOp l).spectrum

★★ Every limit of weights is in the spectrum. The basis vectors are approximate eigenvectors there, so no bounded inverse can exist: it would have to stretch a unit vector by more than its own norm.

theorem HilbertBasis.spectrum_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) : (e.diagOp l).spectrum = closure (Set.range fun (i : ι) => ↑(l i))

★★★ The spectrum of a diagonal operator is the closure of its weight set. Every weight is an eigenvalue, every limit of weights is a spectral value, and nothing else is: off the closure the reciprocal weights assemble a bounded inverse. With isSelfAdjoint_diagOp this is the spectral picture of a self-adjoint operator with a prescribed spectrum.

theorem HilbertBasis.mem_spectrum_diagOp {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (e : HilbertBasis ι 𝕜 E) (l : ι → ℝ) (i : ι) : ↑(l i) ∈ (e.diagOp l).spectrum

★ Every weight is an eigenvalue, hence in the spectrum.