A bounded symmetric perturbation keeps self-adjointness and the domain

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #64(ii), the second of the three pieces that row records itself as waiting on.

★★★ IsSelfAdjoint.addCLM — T + V is self-adjoint on dom T when T is self-adjoint and V is a bounded symmetric operator: the bounded case of Kato–Rellich, which is what gives H₀ + V for a bounded real potential. Behind it:

• LinearPMap.addCLM — the sum, with domain exactly dom T (Mathlib's + on LinearPMap intersects domains, so T + V.toPMap ⊤ has domain dom T ⊓ ⊤, which is equal to dom T but not syntactically it; a perturbation statement wants the domain unchanged on the nose);
• ★★★ LinearPMap.adjoint_addCLM — the adjoint is perturbed the same way, (T + V)† = T† + V, which is the general statement and does not need T self-adjoint;
• ★★ LinearPMap.addCLM_adjointDomain — the adjoint's domain does not move at all, and this needs only boundedness of V, not symmetry: x ↦ ⟪y, V x⟫ is continuous for every y, so it cannot affect whether x ↦ ⟪y, T x⟫ is.

Why the domain is the whole content

Symmetry of T + V is three lines and says nothing: the issue with an unbounded operator is always maximality — that the adjoint has no larger domain. addCLM_adjointDomain is where that is settled, and it is settled by continuity of a bounded functional rather than by any estimate. This is exactly why the bounded case is elementary and the Kato–Rellich theorem proper (a perturbation that is merely relatively bounded, with relative bound < 1) is not: there the domain argument needs the resolvent and a Neumann series, and nothing here covers it.

Honest scope

⚠️ Bounded, not relatively bounded. V is a ContinuousLinearMap. The Kato–Rellich theorem for T-bounded perturbations with relative bound < 1 — the version that covers Coulomb potentials — is a different theorem and is not proved here.

⚠️ No semiboundedness, no form sums. Nothing about KLMN/quadratic forms, which is how potentials that are not operator-bounded are handled.

⚠️ Symmetric is taken as the hypothesis, in the form LinearMap.IsSymmetric, rather than IsSelfAdjoint for a ContinuousLinearMap: they agree for a bounded operator on a complete space, and the symmetric form is what a consumer actually discharges.

References: LinearPMapConj.lean (#64(i), the unitary conjugation), MultiplicationOperator.lean (mulCLM, the bounded multiplication operators this is for), Mathlib/Analysis/InnerProductSpace/LinearPMap.lean (adjoint), Mathlib/Analysis/InnerProductSpace/Symmetric.lean (LinearMap.IsSymmetric); specs/BACKLOG.md #64.

The perturbed operator

def LinearPMap.addCLM {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : E →ₗ.[𝕜] E

T + V for a bounded V, with domain exactly dom T.

Equations

• T.addCLM V = { domain := T.domain, toFun := T.toFun + ↑V ∘ₗ T.domain.subtype }

@[simp]

theorem LinearPMap.addCLM_domain {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : (T.addCLM V).domain = T.domain

theorem LinearPMap.addCLM_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) (x : ↥T.domain) : ↑(T.addCLM V) x = ↑T x + V ↑x

theorem LinearPMap.dense_addCLM_domain {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) (hT : Dense ↑T.domain) : Dense ↑(T.addCLM V).domain

The perturbation does not move the domain, so density is inherited.

The adjoint's domain does not move

This is the content, and it needs only that V is bounded.

theorem LinearPMap.continuous_inner_apply_clm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) (y : E) : Continuous fun (x : ↥T.domain) => inner 𝕜 y (V ↑x)

The functional a bounded perturbation adds is continuous outright.

theorem LinearPMap.addCLM_adjointDomain {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : (T.addCLM V).adjointDomain = T.adjointDomain

★★ The adjoint's domain is unchanged by a bounded perturbation.

theorem LinearPMap.adjoint_addCLM {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) (hV : (↑V).IsSymmetric) (hT : Dense ↑T.domain) : (T.addCLM V).adjoint = T.adjoint.addCLM V

★★★ The adjoint is perturbed the same way: (T + V)† = T† + V, for any bounded symmetric V and any densely defined T. Self-adjointness of T is not needed.

theorem IsSelfAdjoint.addCLM {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ.[𝕜] E} (hT : IsSelfAdjoint T) (V : E →L[𝕜] E) (hV : (↑V).IsSymmetric) : IsSelfAdjoint (T.addCLM V)

★★★ A bounded symmetric perturbation preserves self-adjointness, on the same domain: the bounded case of Kato–Rellich, and what gives H₀ + V for a bounded real potential.