Invariant submodules of operator exponentials

This file characterizes the closed submodules preserved by every operator in the one-parameter family exp (t A). Over a characteristic-zero nontrivially normed field, a closed submodule is preserved by this entire family exactly when it is preserved by its infinitesimal generator A.

This equivalence lets consumers replace preservation by the full exponential family with the single infinitesimal condition that A preserves the submodule.

Main results

• ContinuousLinearMap.forall_exp_smul_mem_invtSubmodule_iff: a closed submodule is invariant under every exp (t A) if and only if it is invariant under A.

theorem ContinuousLinearMap.forall_exp_smul_mem_invtSubmodule_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [ContinuousSMul ℚ 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X] (A : X →L[𝕜] X) {S : Submodule 𝕜 X} (hS : IsClosed ↑S) : (∀ (t : 𝕜), S ∈ Module.End.invtSubmodule ↑(NormedSpace.exp (t • A))) ↔ S ∈ Module.End.invtSubmodule ↑A

A closed submodule is invariant under every exponential exp (t A) if and only if it is invariant under the bounded operator A.