Domains of the iterates of a partially defined linear map

A partially defined linear map A : E →ₗ.[R] E cannot in general be composed with itself: LinearPMap.comp asks for A x ∈ D(A) at every x ∈ D(A), which is exactly what fails for an unbounded operator. What always makes sense is the domain of the n-th iterate,

D(A⁰) = E, D(Aⁿ⁺¹) = {x ∈ D(A) | A x ∈ D(Aⁿ)},

the largest submodule on which A may be applied n times in succession. This file defines it and develops its elementary structure: it shrinks as n grows, D(A¹) is D(A), and A maps D(Aⁿ⁺¹) into D(Aⁿ).

The intended consumer is the theory of strongly continuous semigroups, where D(Aⁿ) for the infinitesimal generator A is the space of vectors whose orbit is n times continuously differentiable, and where the density of every D(Aⁿ) is the standard regularisation statement.

Main declarations

• TauCeti.domainPow: the submodule D(Aⁿ).
• TauCeti.mem_domainPow_succ: the recursive membership criterion defining it.
• TauCeti.domainPow_antitone: D(Aⁿ) decreases with n.
• TauCeti.apply_mem_domainPow: A maps D(Aⁿ⁺¹) into D(Aⁿ).

Tau Ceti puts every declaration under namespace TauCeti, so a name in the LinearPMap namespace could not be reached by generalized field notation anyway; these therefore live in the root TauCeti namespace and are written out as domainPow A n.

def TauCeti.domainPow {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) : ℕ → Submodule R E

The domain D(Aⁿ) of the n-th iterate of a partially defined linear map A: the submodule of vectors to which A may be applied n times in succession.

Equations

• TauCeti.domainPow A 0 = ⊤
• TauCeti.domainPow A n.succ = Submodule.map A.domain.subtype (Submodule.comap A.toFun (TauCeti.domainPow A n))

@[simp]

theorem TauCeti.domainPow_zero {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) : domainPow A 0 = ⊤

theorem TauCeti.domainPow_succ {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) (n : ℕ) : domainPow A (n + 1) = Submodule.map A.domain.subtype (Submodule.comap A.toFun (domainPow A n))

@[simp]

theorem TauCeti.mem_domainPow_succ {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {A : E →ₗ.[R] E} {n : ℕ} {x : E} : x ∈ domainPow A (n + 1) ↔ ∃ (hx : x ∈ A.domain), ↑A ⟨x, hx⟩ ∈ domainPow A n

Membership in D(Aⁿ⁺¹): a vector of D(A) whose image under A lies in D(Aⁿ).

@[simp]

theorem TauCeti.domainPow_one {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) : domainPow A 1 = A.domain

theorem TauCeti.domainPow_succ_le {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) (n : ℕ) : domainPow A (n + 1) ≤ domainPow A n

theorem TauCeti.domainPow_antitone {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) : Antitone (domainPow A)

The iterated domains D(Aⁿ) decrease as the iteration count increases.

theorem TauCeti.domainPow_succ_le_domain {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (A : E →ₗ.[R] E) (n : ℕ) : domainPow A (n + 1) ≤ A.domain

theorem TauCeti.apply_mem_domainPow {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {A : E →ₗ.[R] E} {n : ℕ} {x : E} (hx : x ∈ domainPow A (n + 1)) : ↑A ⟨x, ⋯⟩ ∈ domainPow A n

A maps D(Aⁿ⁺¹) into D(Aⁿ).