Documentation

TauCeti.LinearAlgebra.LinearPMap.SmulSub

The shift c • x - A x of a partial linear map as a linear map on its domain #

For a partial linear map A : E →ₗ.[R] E and a scalar c, the shift x ↦ c • x - A x is a linear map from the domain of A to E. Bundling it (LinearPMap.smulSub) gives access to the LinearMap API, in particular to its range as a submodule, for arguments about resolvents, deficiency shifts and dissipativity, where surjectivity or density of this range is the question. Up to sign it is the scalar shift TauCeti.LinearPMap.subScalar A c = A - c • 1 of TauCeti.LinearAlgebra.LinearPMap.Shift, regarded as a linear map on the domain (smulSub_apply_eq_neg_subScalar), so results about the range of either form transfer to the other.

Main declarations #

source
def LinearPMap.smulSub {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] (c : R) (A : E →ₗ.[R] E) :
↥A.domain →ₗ[R] E

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

Equations
Instances For
    source
    @[simp]
    theorem LinearPMap.smulSub_apply {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] (c : R) (A : E →ₗ.[R] E) (x : ↥A.domain) :
    (smulSub c A) x = c • ↑x - ↑A x
    source
    theorem LinearPMap.smulSub_apply_eq_neg_subScalar {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] (c : R) (A : E →ₗ.[R] E) (x : ↥A.domain) :
    (smulSub c A) x = -↑(TauCeti.LinearPMap.subScalar A c) ⟨↑x, ⋯⟩

    The bundled shift c • x - A x is the negative of the scalar shift subScalar A c = A - c • 1 of the same domain, pointwise.

    source
    theorem LinearPMap.coe_range_smulSub {R : Type u_1} {E : Type u_2} [CommRing R] [AddCommGroup E] [Module R E] (c : R) (A : E →ₗ.[R] E) :
    ↑(smulSub c A).range = Set.range fun (x : ↥A.domain) => c • ↑x - ↑A x

    The range of the bundled shift is the range of the shift.