The resolvent raises the order of an iterated domain

At a point lambda of the resolvent set of an unbounded operator A, the resolvent R(lambda, A) is a right inverse of lambda • I - A, so A R(lambda) y = lambda R(lambda) y - y for every y. Reading that identity as a recursion turns a single regularity step, R(lambda) y ∈ D(A), into the statement that R(lambda) maps D(Aⁿ) into D(Aⁿ⁺¹); in particular R(lambda)ⁿ lands in D(Aⁿ).

These are the regularising maps behind the density of the iterated domains D(Aⁿ), since lambdaⁿ R(lambda)ⁿ converges strongly to the identity for a generator.

Main results

• TauCeti.resolvent_mem_domainPow_succ: R(lambda) maps D(Aⁿ) into D(Aⁿ⁺¹).
• TauCeti.resolvent_pow_mem_domainPow: R(lambda)ⁿ maps X into D(Aⁿ).

theorem TauCeti.resolvent_mem_domainPow_succ {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda : ℝ} (h : lambda ∈ A.resolventSet) {n : ℕ} {x : X} (hx : x ∈ domainPow A n) : (A.resolvent lambda) x ∈ domainPow A (n + 1)

The resolvent raises the order of an iterated domain by one: it maps D(Aⁿ) into D(Aⁿ⁺¹).

theorem TauCeti.resolvent_pow_mem_domainPow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda : ℝ} (h : lambda ∈ A.resolventSet) (n : ℕ) (x : X) : (A.resolvent lambda ^ n) x ∈ domainPow A n

The n-th power of the resolvent regularises every vector to order n: it maps X into D(Aⁿ).