Relatively bounded partial linear maps

A partial linear map V is relatively bounded with respect to a partial linear map A, with constants a and b, when the domain of A lies in the domain of V and

‖V x‖ ≤ a * ‖x‖ + b * ‖A x‖ for every x in the domain of A.

This is the size condition of perturbation theory for unbounded operators: the perturbation is controlled by the graph of A rather than by ‖x‖ alone, and the Kato–Rellich theorem asks for b < 1. The infimum of the admissible b is Kato's A-bound of V.

This file sets up the predicate and its elementary calculus: the zero map is relatively bounded with constants 0, 0; the constants may be increased; relative bounds add under sums and differences, scale under scalar multiplication and are unchanged by negation; and a bounded operator on the whole space is relatively bounded with constants ‖T‖, 0. Sums and differences use Mathlib's addition of partial linear maps, whose domain is the intersection of the two domains.

Main declarations

• LinearPMap.IsRelativelyBounded V A a b: V is A-bounded with constants a, b.
• LinearPMap.IsRelativelyBounded.mono: increasing the constants.
• LinearPMap.IsRelativelyBounded.domain_add: the domain of A + V is the domain of A.
• LinearPMap.IsRelativelyBounded.add, .sub, .neg, .smul: the linear calculus.
• LinearPMap.isRelativelyBounded_zero, ContinuousLinearMap.isRelativelyBounded_toPMap: the zero map and bounded operators.

References

• T. Kato, Perturbation Theory for Linear Operators, 2nd ed., Springer (1976), §IV.1.1.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press (1975), §X.2.

structure LinearPMap.IsRelativelyBounded {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (V : E →ₗ.[𝕜] G) (A : E →ₗ.[𝕜] F) (a b : ℝ) : Prop

A partial linear map V is relatively bounded with respect to A, with constants a and b, when A.domain ≤ V.domain and ‖V x‖ ≤ a * ‖x‖ + b * ‖A x‖ for every x in the domain of A.

• domain_le : A.domain ≤ V.domain

  The domain of A lies in the domain of V.

• norm_apply_le (x : ↥A.domain) : ‖↑V ⟨↑x, ⋯⟩‖ ≤ a * ‖↑x‖ + b * ‖↑A x‖

  The relative bound ‖V x‖ ≤ a * ‖x‖ + b * ‖A x‖ on the domain of A.

theorem LinearPMap.IsRelativelyBounded.mono {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V : E →ₗ.[𝕜] G} {A : E →ₗ.[𝕜] F} {a b a' b' : ℝ} (h : V.IsRelativelyBounded A a b) (ha : a ≤ a') (hb : b ≤ b') : V.IsRelativelyBounded A a' b'

A relative bound holds at any larger pair of constants.

theorem LinearPMap.IsRelativelyBounded.domain_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {a b : ℝ} {V A : E →ₗ.[𝕜] F} (h : V.IsRelativelyBounded A a b) : (A + V).domain = A.domain

If V is relatively bounded with respect to A, then A + V has the same domain as A.

theorem LinearPMap.IsRelativelyBounded.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V W : E →ₗ.[𝕜] G} {A : E →ₗ.[𝕜] F} {a b a' b' : ℝ} (hV : V.IsRelativelyBounded A a b) (hW : W.IsRelativelyBounded A a' b') : (V + W).IsRelativelyBounded A (a + a') (b + b')

Relative bounds add under the sum of two partial linear maps.

theorem LinearPMap.IsRelativelyBounded.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V : E →ₗ.[𝕜] G} {A : E →ₗ.[𝕜] F} {a b : ℝ} (h : V.IsRelativelyBounded A a b) : (-V).IsRelativelyBounded A a b

Negation does not change a relative bound.

theorem LinearPMap.IsRelativelyBounded.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V W : E →ₗ.[𝕜] G} {A : E →ₗ.[𝕜] F} {a b a' b' : ℝ} (hV : V.IsRelativelyBounded A a b) (hW : W.IsRelativelyBounded A a' b') : (V - W).IsRelativelyBounded A (a + a') (b + b')

Relative bounds add under the difference of two partial linear maps.

theorem LinearPMap.IsRelativelyBounded.smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V : E →ₗ.[𝕜] G} {A : E →ₗ.[𝕜] F} {a b : ℝ} (h : V.IsRelativelyBounded A a b) (c : 𝕜) : (c • V).IsRelativelyBounded A (‖c‖ * a) (‖c‖ * b)

A scalar multiple c • V is relatively bounded with the constants scaled by ‖c‖.

theorem LinearPMap.isRelativelyBounded_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (A : E →ₗ.[𝕜] F) : IsRelativelyBounded 0 A 0 0

The zero map is relatively bounded with constants 0, 0.

theorem ContinuousLinearMap.isRelativelyBounded_toPMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (T : E →L[𝕜] G) (A : E →ₗ.[𝕜] F) : ((↑T).toPMap ⊤).IsRelativelyBounded A ‖T‖ 0

A bounded operator T on the whole space, viewed as a partial linear map with domain ⊤, is relatively bounded with respect to every partial linear map, with constants ‖T‖, 0.