Shifts of a partial linear map on a normed space

For a partial linear map A on a normed space and a scalar c, this file studies the shift x ↦ c • x - A x (bundled as LinearPMap.smulSub in TauCeti.LinearAlgebra.LinearPMap.SmulSub) under a lower bound. A shift bounded below by a multiple of ‖x‖ is injective; a shift bounded below by a multiple of the graph norm max ‖x‖ ‖A x‖ of a closed A has closed range, because it is then an antilipschitz map on the complete graph of A. These are the common cores of the injectivity of λ - A for a dissipative A and of the closed-range property of the nonreal shifts of a closed symmetric A.

Main results

• LinearPMap.smul_sub_injective_of_norm_le: a shift bounded below by a multiple of ‖x‖ is injective.
• LinearPMap.graphSmulSub: the shift as a continuous linear map on the graph of A, with graphSmulSub_apply and range_graphSmulSub.
• LinearPMap.isClosed_range_smul_sub_of_graph_norm_le: a shift of a closed partial linear map that is bounded below by a multiple of the graph norm has closed range.

theorem LinearPMap.smul_sub_injective_of_norm_le {𝕜 : Type u_1} {E : Type u_2} [CommRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] {A : E →ₗ.[𝕜] E} {c : 𝕜} {K : ℝ} (hK : 0 < K) (h : ∀ (x : ↥A.domain), K * ‖↑x‖ ≤ ‖c • ↑x - ↑A x‖) : Function.Injective fun (x : ↥A.domain) => c • ↑x - ↑A x

A shift x ↦ c • x - A x dominating K * ‖x‖ for some K > 0 is injective, being antilipschitz.

def LinearPMap.graphSmulSub {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : 𝕜) : ↥A.graph →L[𝕜] E

The shift x ↦ c • x - A x, as a continuous linear map on the graph of A.

Equations

• A.graphSmulSub c = (c • ContinuousLinearMap.fst 𝕜 E E - ContinuousLinearMap.snd 𝕜 E E).domRestrict A.graph

@[simp]

theorem LinearPMap.graphSmulSub_apply {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : 𝕜) (z : ↥A.graph) : (A.graphSmulSub c) z = c • (↑z).1 - (↑z).2

theorem LinearPMap.range_graphSmulSub {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : 𝕜) : Set.range ⇑(A.graphSmulSub c) = Set.range fun (x : ↥A.domain) => c • ↑x - ↑A x

The range of the graph shift is the range of the shift.

theorem LinearPMap.norm_le_mul_norm_graphSmulSub {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {c : 𝕜} {K : NNReal} (hbound : ∀ (x : ↥A.domain), max ‖↑x‖ ‖↑A x‖ ≤ ↑K * ‖c • ↑x - ↑A x‖) (z : ↥A.graph) : ‖↑z‖ ≤ ↑K * ‖(A.graphSmulSub c) z‖

A lower bound for the shift in terms of the graph norm max ‖x‖ ‖A x‖ is a lower bound for the graph shift in terms of the norm of the graph.

theorem LinearPMap.isClosed_range_smul_sub_of_graph_norm_le {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} (hcl : A.IsClosed) {c : 𝕜} {K : NNReal} (hbound : ∀ (x : ↥A.domain), max ‖↑x‖ ‖↑A x‖ ≤ ↑K * ‖c • ↑x - ↑A x‖) : _root_.IsClosed (Set.range fun (x : ↥A.domain) => c • ↑x - ↑A x)

A shift bounded below in the graph norm has closed range. If A is closed and max ‖x‖ ‖A x‖ ≤ K * ‖c • x - A x‖ on the domain, then the range of x ↦ c • x - A x is closed: the graph shift is an antilipschitz map on the complete graph of A.