Scalar shifts of partial linear maps

For a partial linear map A, subtracting the scalar operator omega I leaves its domain unchanged. This file develops the generic construction and its basic normalization API.

Main results

• TauCeti.LinearPMap.subScalar: the operator A - omega I on the domain of A.
• TauCeti.LinearPMap.subScalar_domain: scalar shifts preserve the domain.
• TauCeti.LinearPMap.subScalar_apply: pointwise evaluation of a scalar shift.
• TauCeti.LinearPMap.vadd_subScalar and TauCeti.LinearPMap.subScalar_vadd: scalar shifts commute with adding a globally defined map, and absorb into it.

def TauCeti.LinearPMap.subScalar {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] (A : X →ₗ.[R] X) (omega : R) : X →ₗ.[R] X

Subtract the scalar operator omega I from an unbounded operator A, without changing its domain.

Equations

• TauCeti.LinearPMap.subScalar A omega = -omega • LinearMap.id +ᵥ A

@[simp]

theorem TauCeti.LinearPMap.subScalar_domain {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] (A : X →ₗ.[R] X) (omega : R) : (subScalar A omega).domain = A.domain

A scalar shift does not change the domain of an unbounded operator.

@[simp]

theorem TauCeti.LinearPMap.subScalar_apply {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] (A : X →ₗ.[R] X) (omega : R) (x : ↥(subScalar A omega).domain) : ↑(subScalar A omega) x = ↑A ⟨↑x, ⋯⟩ - omega • ↑x

Pointwise evaluation of the shifted operator A - omega I.

@[simp]

theorem TauCeti.LinearPMap.subScalar_zero {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] (A : X →ₗ.[R] X) : subScalar A 0 = A

The zero scalar shift is the original operator.

@[simp]

theorem TauCeti.LinearPMap.subScalar_subScalar {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] (A : X →ₗ.[R] X) (omega mu : R) : subScalar (subScalar A omega) mu = subScalar A (omega + mu)

Successive scalar shifts add their parameters.

@[simp]

theorem TauCeti.LinearPMap.vadd_subScalar {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] {A : X →ₗ.[R] X} (f : X →ₗ[R] X) (omega : R) : f +ᵥ subScalar A omega = subScalar (f +ᵥ A) omega

A globally defined linear summand and a scalar shift commute: adding the map to A and then subtracting omega I gives the same operator either way round.

@[simp]

theorem TauCeti.LinearPMap.subScalar_vadd {R : Type u_1} {X : Type u_2} [CommRing R] [AddCommGroup X] [Module R X] {A : X →ₗ.[R] X} (f : X →ₗ[R] X) (omega : R) : subScalar (f +ᵥ A) omega = (f - omega • LinearMap.id) +ᵥ A

A scalar shift of a globally defined linear perturbation absorbs into the perturbing map. This is the form in which the domain of a shifted perturbation is visibly the domain of A.