Domain-aware infrastructure for partial linear maps

Reusable algebra for unbounded operators represented canonically by Mathlib's LinearPMap: domain transport, extension, symmetry, graph norms, relative bounds, and elementary real resolvent predicates.

The declarations deliberately take raw partial maps. Closedness, dense domain, and self-adjointness are separate hypotheses supplied by the theorem that needs them; they are not bundled into a parallel operator structure.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/SpectralTheory/ClosedOperator/Basic.lean.
• Extraction class: representation migration. The original declarations were methods of a bundled ClosedOperator record -- a LinearPMap with dense domain and closed graph as fields, since deleted downstream; this module restates their reusable content directly over Mathlib LinearPMap.
• Spectra influence: none. This module imports only Mathlib.

theorem TauCeti.LinearPMap.isClosed_iff_range_isClosed {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (f : E →ₗ.[𝕜] F) : f.IsClosed ↔ IsClosed (Set.range fun (x : ↥f.domain) => (↑x, ↑f x))

LinearPMap.IsClosed is stated on the graph, while the canonical reducing-restriction API states closedness as a range. The two are the same set, so this is a reindexing lemma used in both directions.

def TauCeti.LinearPMap.SameDomain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A B : E →ₗ.[𝕜] E) : Prop

Two partial linear maps have the same operator domain.

Equations

• TauCeti.LinearPMap.SameDomain A B = (A.domain = B.domain)

theorem TauCeti.LinearPMap.SameDomain.refl {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : SameDomain A A

Equality of partial-map domains is reflexive.

theorem TauCeti.LinearPMap.SameDomain.symm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B : E →ₗ.[𝕜] E} (h : SameDomain A B) : SameDomain B A

Equality of partial-map domains is symmetric.

theorem TauCeti.LinearPMap.SameDomain.trans {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B C : E →ₗ.[𝕜] E} (hAB : SameDomain A B) (hBC : SameDomain B C) : SameDomain A C

Equality of partial-map domains is transitive.

def TauCeti.LinearPMap.MapsDomainTo {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (X : F →L[𝕜] E) : Prop

A bounded map sends the domain of B into the domain of A.

Equations

• TauCeti.LinearPMap.MapsDomainTo A B X = ∀ (x : ↥B.domain), X ↑x ∈ A.domain

theorem TauCeti.LinearPMap.MapsDomainTo.id {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : MapsDomainTo A A (ContinuousLinearMap.id 𝕜 E)

The identity bounded map preserves every partial-map domain.

theorem TauCeti.LinearPMap.MapsDomainTo.comp {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {G : Type u_1} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {C : G →ₗ.[𝕜] G} {X : F →L[𝕜] E} {Y : G →L[𝕜] F} (hX : MapsDomainTo A B X) (hY : MapsDomainTo B C Y) : MapsDomainTo A C (X ∘SL Y)

Domain transport composes with bounded maps.

def TauCeti.LinearPMap.InvariantSubspace {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) : Prop

A subspace is invariant under a partial linear map on its domain.

Equations

• TauCeti.LinearPMap.InvariantSubspace A U = ∀ (x : ↥A.domain), ↑x ∈ U → ↑A x ∈ U

def TauCeti.LinearPMap.ReducesSubspace {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Prop

A subspace reduces a partial linear map when both orthogonal projections preserve its domain and both summands are invariant.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LinearPMap.ReducesSubspace.of_components {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h₁ : ∀ (x : ↥A.domain), U.starProjection ↑x ∈ A.domain) (h₂ : ∀ (x : ↥A.domain), Uᗮ.starProjection ↑x ∈ A.domain) (h₃ : InvariantSubspace A U) (h₄ : InvariantSubspace A Uᗮ) : ReducesSubspace A U

Build a ReducesSubspace from its four components. The definition is a conjunction whose body is not exposed across module boundaries, so this is the supported way for a consumer to construct one.

theorem TauCeti.LinearPMap.ReducesSubspace.projection_mem_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : ReducesSubspace A U) (x : ↥A.domain) : U.starProjection ↑x ∈ A.domain

The projection onto a reducing subspace preserves the partial-map domain.

theorem TauCeti.LinearPMap.ReducesSubspace.orthogonalProjection_mem_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : ReducesSubspace A U) (x : ↥A.domain) : Uᗮ.starProjection ↑x ∈ A.domain

The complementary projection of a reducing subspace preserves the domain.

theorem TauCeti.LinearPMap.ReducesSubspace.invariant {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : ReducesSubspace A U) : InvariantSubspace A U

The selected summand of a reducing subspace is invariant.

theorem TauCeti.LinearPMap.ReducesSubspace.orthogonal_invariant {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : ReducesSubspace A U) : InvariantSubspace A Uᗮ

The complementary summand of a reducing subspace is invariant.

theorem TauCeti.LinearPMap.ReducesSubspace.orthogonal {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : ReducesSubspace A U) : ReducesSubspace A Uᗮ

Orthogonal complementation preserves the reducing-subspace property.

def TauCeti.LinearPMap.reducingRestrictionDomain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) : Submodule 𝕜 ↥U

The operator domain inside a reducing subspace.

Equations

• TauCeti.LinearPMap.reducingRestrictionDomain A U = { carrier := {x : ↥U | ↑x ∈ A.domain}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.LinearPMap.mem_reducingRestrictionDomain_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) (x : ↥U) : x ∈ reducingRestrictionDomain A U ↔ ↑x ∈ A.domain

Membership in the restricted domain is membership of the ambient vector in A.domain: restricting the domain to U adds no condition beyond lying in U, which the subtype already carries.

def TauCeti.LinearPMap.reducingRestrictionDomainToAmbient {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) (x : ↥(reducingRestrictionDomain A U)) : ↥A.domain

A restricted-domain vector viewed in the ambient partial-map domain.

Equations

• TauCeti.LinearPMap.reducingRestrictionDomainToAmbient A U x = ⟨↑↑x, ⋯⟩

@[simp]

theorem TauCeti.LinearPMap.reducingRestrictionDomainToAmbient_coe {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) (x : ↥(reducingRestrictionDomain A U)) : ↑(reducingRestrictionDomainToAmbient A U x) = ↑↑x

Viewing a restricted-domain vector in the ambient domain does not move it. The two subtypes differ only in which membership proof they carry.

def TauCeti.LinearPMap.reducingRestrictionLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) : ↥(reducingRestrictionDomain A U) →ₗ[𝕜] ↥U

Action of a partial map restricted to a reducing subspace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LinearPMap.coe_reducingRestrictionLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (x : ↥(reducingRestrictionDomain A U)) : ↑((reducingRestrictionLinearMap A U hred) x) = ↑A (reducingRestrictionDomainToAmbient A U x)

The restricted map acts by the ambient one: A|_U x = A x, read through the two coercions. This is where ReducesSubspace earns its keep — it is what makes A x land back in U so the corestriction typechecks.

noncomputable def TauCeti.LinearPMap.projectDomainToReducingRestriction {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (x : ↥A.domain) : ↥(reducingRestrictionDomain A U)

Projection of an ambient domain vector into the restricted domain.

Equations

• TauCeti.LinearPMap.projectDomainToReducingRestriction A U hred x = ⟨⟨U.starProjection ↑x, ⋯⟩, ⋯⟩

@[simp]

theorem TauCeti.LinearPMap.coe_projectDomainToReducingRestriction {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (x : ↥A.domain) : ↑↑(projectDomainToReducingRestriction A U hred x) = U.starProjection ↑x

Projecting an ambient domain vector into the restricted domain is the orthogonal projection onto U. It stays in the domain because A reduces U.

noncomputable def TauCeti.LinearPMap.reducingRestriction {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) : ↥U →ₗ.[𝕜] ↥U

The partial map induced on a reducing subspace. Density and closedness are properties supplied separately by the theorem using this construction.

Equations

• TauCeti.LinearPMap.reducingRestriction A U hred = { domain := TauCeti.LinearPMap.reducingRestrictionDomain A U, toFun := TauCeti.LinearPMap.reducingRestrictionLinearMap A U hred }

@[simp]

theorem TauCeti.LinearPMap.reducingRestriction_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) : (reducingRestriction A U hred).domain = reducingRestrictionDomain A U

The restricted partial map has the restricted domain, definitionally.

theorem TauCeti.LinearPMap.mem_reducingRestriction_domain_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (x : ↥U) : x ∈ (reducingRestriction A U hred).domain ↔ ↑x ∈ A.domain

Membership in the restricted domain, stated without naming the intermediate domain submodule. This is the form a consumer outside this module can use: the restricted operator's domain is U-vectors that already lay in A.domain.

theorem TauCeti.LinearPMap.coe_reducingRestriction_apply {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (x : ↥U) (hx : ↑x ∈ A.domain) : ↑(↑(reducingRestriction A U hred) ⟨x, ⋯⟩) = ↑A ⟨↑x, hx⟩

The reducing restriction acts by the ambient partial map, read through the two coercions and indexed by an ambient-domain proof rather than by the restricted domain's subtype. coe_reducingRestrictionLinearMap says the same about the underlying linear map; this is the partial-map form, and it is what a consumer needs to compute with a restriction it did not build.

theorem TauCeti.LinearPMap.reducingRestriction_dense {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (hA : Dense ↑A.domain) : Dense ↑(reducingRestriction A U hred).domain

A dense partial-map domain remains dense after restriction to a reducing subspace.

theorem TauCeti.LinearPMap.reducingRestriction_closedGraph {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (hA : IsClosed (Set.range fun (x : ↥A.domain) => (↑x, ↑A x))) : IsClosed (Set.range fun (x : ↥(reducingRestriction A U hred).domain) => (↑x, ↑(reducingRestriction A U hred) x))

Closedness of the graph is preserved by restriction to a reducing subspace. The hypothesis is stated as a graph range to make it directly applicable to compatibility records as well as raw partial maps.

theorem TauCeti.LinearPMap.mem_reducingRestriction_adjoint_domain_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [CompleteSpace E] [CompleteSpace ↥U] (hred : ReducesSubspace A U) (y : ↥U) : y ∈ (reducingRestriction A U hred).adjoint.domain ↔ ↑y ∈ A.adjoint.domain

Adjoint-domain membership of a reducing restriction is exactly ambient adjoint-domain membership for the included vector.

theorem TauCeti.LinearPMap.reducingRestriction_isSymmetric {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (hred : ReducesSubspace A U) (hA : ∀ (x y : ↥A.domain), inner 𝕜 (↑A x) ↑y = inner 𝕜 (↑x) (↑A y)) (x y : ↥(reducingRestriction A U hred).domain) : inner 𝕜 (↑(reducingRestriction A U hred) x) ↑y = inner 𝕜 (↑x) (↑(reducingRestriction A U hred) y)

Symmetry passes to a reducing restriction of a partial map.

structure TauCeti.LinearPMap.BoundedExtension {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (D : Submodule 𝕜 F) (T : ↥D →ₗ[𝕜] E) : Type (max v w)

A linear map on a submodule has a bounded extension to the ambient space.

• operator : F →L[𝕜] E

  The bounded ambient extension agreeing with the specified map on its submodule.

• agrees (x : ↥D) : self.operator ↑x = T x

def TauCeti.LinearPMap.Extends {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A B : E →ₗ.[𝕜] E) : Prop

Extension relation for partial linear maps.

Equations

• TauCeti.LinearPMap.Extends A B = ∃ (hdom : A.domain ≤ B.domain), ∀ (x : ↥A.domain), ↑B ⟨↑x, ⋯⟩ = ↑A x

theorem TauCeti.LinearPMap.Extends.refl {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Extends A A

Every partial linear map extends itself.

theorem TauCeti.LinearPMap.Extends.trans {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A B C : E →ₗ.[𝕜] E} (hAB : Extends A B) (hBC : Extends B C) : Extends A C

Extension of partial linear maps is transitive.

def TauCeti.LinearPMap.pullbackDomain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) : Submodule 𝕜 E

Domain obtained by pulling a partial-map domain back through a continuous linear equivalence.

Equations

• TauCeti.LinearPMap.pullbackDomain A e = Submodule.comap (↑↑e) A.domain

@[simp]

theorem TauCeti.LinearPMap.mem_pullbackDomain_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (x : E) : x ∈ pullbackDomain A e ↔ e x ∈ A.domain

x lies in the pulled-back domain exactly when e x lies in the original one — the pullback domain is the preimage, so the condition is on the image.

def TauCeti.LinearPMap.pullbackDomainToOriginal {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) : ↥(pullbackDomain A e) →ₗ[𝕜] ↥A.domain

A vector in a pulled-back domain, transported to the original domain.

Equations

• TauCeti.LinearPMap.pullbackDomainToOriginal A e = { toFun := fun (x : ↥(TauCeti.LinearPMap.pullbackDomain A e)) => ⟨e ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.LinearPMap.pullbackDomainToOriginal_coe {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (x : ↥(pullbackDomain A e)) : ↑((pullbackDomainToOriginal A e) x) = e ↑x

Transporting a pulled-back domain vector applies e. Unlike the reducing restriction, this map genuinely moves the vector.

def TauCeti.LinearPMap.pullbackLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) : ↥(pullbackDomain A e) →ₗ[𝕜] E

Action of the partial map pulled back through a continuous linear equivalence.

Equations

• TauCeti.LinearPMap.pullbackLinearMap A e = ↑↑e.symm ∘ₗ A.toFun ∘ₗ TauCeti.LinearPMap.pullbackDomainToOriginal A e

@[simp]

theorem TauCeti.LinearPMap.pullbackLinearMap_apply {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (x : ↥(pullbackDomain A e)) : (pullbackLinearMap A e) x = e.symm (↑A ((pullbackDomainToOriginal A e) x))

The pulled-back action is e⁻¹ ∘ A ∘ e: push forward by e, apply A, pull back by e⁻¹. Conjugation, written on the domain subtypes.

noncomputable def TauCeti.LinearPMap.pullback {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) : E →ₗ.[𝕜] E

Pull a partial map back through a continuous linear equivalence. Density and graph closedness are separate properties of the resulting partial map.

Equations

• TauCeti.LinearPMap.pullback A e = { domain := TauCeti.LinearPMap.pullbackDomain A e, toFun := TauCeti.LinearPMap.pullbackLinearMap A e }

@[simp]

theorem TauCeti.LinearPMap.pullback_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) : (pullback A e).domain = pullbackDomain A e

The pulled-back partial map has the pulled-back domain, definitionally.

theorem TauCeti.LinearPMap.pullback_dense {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (hA : Dense ↑A.domain) : Dense ↑(pullback A e).domain

Pullback through a continuous linear equivalence preserves a dense domain.

theorem TauCeti.LinearPMap.pullback_closedGraph {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (hA : IsClosed (Set.range fun (x : ↥A.domain) => (↑x, ↑A x))) : IsClosed (Set.range fun (x : ↥(pullback A e).domain) => (↑x, ↑(pullback A e) x))

Pullback through a continuous linear equivalence preserves graph closedness.

def TauCeti.LinearPMap.IsUnitaryOperator {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (W : E →L[𝕜] E) : Prop

A bounded operator is unitary when it is norm preserving and surjective.

Equations

• TauCeti.LinearPMap.IsUnitaryOperator W = ((∀ (x : E), ‖W x‖ = ‖x‖) ∧ Function.Surjective ⇑W)

def TauCeti.LinearPMap.UnitaryEquivalent {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A B : E →ₗ.[𝕜] E) (W Winv : E →L[𝕜] E) : Prop

Two partial maps are unitarily equivalent when mutually inverse unitary maps transport both domains and both actions.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LinearPMap.pullback_unitaryEquivalent {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (e : E ≃L[𝕜] E) (he : IsUnitaryOperator ↑e) : UnitaryEquivalent (pullback A e) A ↑e ↑e.symm

Pullback through a unitary equivalence is unitarily equivalent to the original partial map.

noncomputable def TauCeti.LinearPMap.directSumDomain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : Submodule 𝕜 (WithLp 2 (E × F))

The explicit product domain of two partial maps, transported to the L² Hilbert direct sum.

Equations

• TauCeti.LinearPMap.directSumDomain A B = Submodule.comap (↑(WithLp.linearEquiv 2 𝕜 (E × F))) (A.domain.prod B.domain)

@[simp]

theorem TauCeti.LinearPMap.mem_directSumDomain_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (z : WithLp 2 (E × F)) : z ∈ directSumDomain A B ↔ z.fst ∈ A.domain ∧ z.snd ∈ B.domain

A vector lies in the direct-sum domain exactly when each coordinate lies in the corresponding domain. The WithLp 2 wrapper carries the Hilbert norm and changes nothing about membership.

def TauCeti.LinearPMap.directSumDomainFst {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (z : ↥(directSumDomain A B)) : ↥A.domain

First coordinate of a direct-sum domain vector.

Equations

• TauCeti.LinearPMap.directSumDomainFst A B z = ⟨(↑z).fst, ⋯⟩

def TauCeti.LinearPMap.directSumDomainSnd {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (z : ↥(directSumDomain A B)) : ↥B.domain

Second coordinate of a direct-sum domain vector.

Equations

• TauCeti.LinearPMap.directSumDomainSnd A B z = ⟨(↑z).snd, ⋯⟩

def TauCeti.LinearPMap.directSumDomainFstLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : ↥(directSumDomain A B) →ₗ[𝕜] ↥A.domain

First-coordinate extraction as a linear map on a direct-sum domain.

Equations

• TauCeti.LinearPMap.directSumDomainFstLinearMap A B = { toFun := TauCeti.LinearPMap.directSumDomainFst A B, map_add' := ⋯, map_smul' := ⋯ }

def TauCeti.LinearPMap.directSumDomainSndLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : ↥(directSumDomain A B) →ₗ[𝕜] ↥B.domain

Second-coordinate extraction as a linear map on a direct-sum domain.

Equations

• TauCeti.LinearPMap.directSumDomainSndLinearMap A B = { toFun := TauCeti.LinearPMap.directSumDomainSnd A B, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def TauCeti.LinearPMap.directSumLinearMap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : ↥(directSumDomain A B) →ₗ[𝕜] WithLp 2 (E × F)

Componentwise partial-map action on a direct-sum domain.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.LinearPMap.directSum {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : WithLp 2 (E × F) →ₗ.[𝕜] WithLp 2 (E × F)

The direct sum of two partial maps. Density and closedness remain separate properties.

Equations

• TauCeti.LinearPMap.directSum A B = { domain := TauCeti.LinearPMap.directSumDomain A B, toFun := TauCeti.LinearPMap.directSumLinearMap A B }

@[simp]

theorem TauCeti.LinearPMap.directSum_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) : (directSum A B).domain = directSumDomain A B

The direct-sum partial map has the direct-sum domain, definitionally.

theorem TauCeti.LinearPMap.directSum_dense {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (hA : Dense ↑A.domain) (hB : Dense ↑B.domain) : Dense ↑(directSum A B).domain

The direct sum of dense partial-map domains is dense.

theorem TauCeti.LinearPMap.directSum_closedGraph {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (hA : IsClosed (Set.range fun (x : ↥A.domain) => (↑x, ↑A x))) (hB : IsClosed (Set.range fun (y : ↥B.domain) => (↑y, ↑B y))) : IsClosed (Set.range fun (z : ↥(directSum A B).domain) => (↑z, ↑(directSum A B) z))

The direct sum of closed partial-map graphs is closed.

def TauCeti.LinearPMap.IsSymmetric {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Prop

A partial linear map is symmetric on its operator domain.

Equations

• TauCeti.LinearPMap.IsSymmetric A = ∀ (x y : ↥A.domain), inner 𝕜 (↑A x) ↑y = inner 𝕜 (↑x) (↑A y)

theorem TauCeti.LinearPMap.isSymmetric_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : IsSymmetric A ↔ ∀ (x y : ↥A.domain), inner 𝕜 (↑A x) ↑y = inner 𝕜 (↑x) (↑A y)

Characteristic form of symmetry for a partial linear map.

This theorem is the public unfolding interface for IsSymmetric. Keep downstream modules on this theorem rather than depending on definitional transparency across module boundaries.

theorem TauCeti.LinearPMap.isSymmetric_of_isSelfAdjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) : IsSymmetric A

A self-adjoint partial map is symmetric on its operator domain.

The converse fails: symmetry compares A with A† only on dom A, while self-adjointness also asserts that the two domains agree.

theorem TauCeti.LinearPMap.reducingRestriction_isSelfAdjoint {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] [CompleteSpace E] [CompleteSpace ↥U] (hred : ReducesSubspace A U) (hDense : Dense ↑A.domain) (hA : IsSelfAdjoint A) : IsSelfAdjoint (reducingRestriction A U hred)

A self-adjoint partial map restricts to a self-adjoint partial map on every reducing subspace.

noncomputable def TauCeti.LinearPMap.graphNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (x : ↥A.domain) : ℝ

Graph norm associated with a partial linear map.

Equations

• TauCeti.LinearPMap.graphNorm A x = √(‖↑x‖ ^ 2 + ‖↑A x‖ ^ 2)

theorem TauCeti.LinearPMap.graphNorm_nonneg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (x : ↥A.domain) : 0 ≤ graphNorm A x

The graph norm is nonnegative.

theorem TauCeti.LinearPMap.graphNorm_sq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (x : ↥A.domain) : graphNorm A x ^ 2 = ‖↑x‖ ^ 2 + ‖↑A x‖ ^ 2

Squaring the graph norm recovers its defining sum of squares.

theorem TauCeti.LinearPMap.norm_coe_le_graphNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (x : ↥A.domain) : ‖↑x‖ ≤ graphNorm A x

The ambient norm is controlled by the graph norm.

theorem TauCeti.LinearPMap.norm_apply_le_graphNorm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (x : ↥A.domain) : ‖↑A x‖ ≤ graphNorm A x

The operator-value norm is controlled by the graph norm.

noncomputable def TauCeti.LinearPMap.addBounded {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : E →ₗ.[𝕜] E

Add a bounded ambient perturbation to a partial map on its original domain. Closedness remains a separate property of the resulting map.

Equations

• TauCeti.LinearPMap.addBounded A V = { domain := A.domain, toFun := A.toFun + (↑V).domRestrict A.domain }

@[simp]

theorem TauCeti.LinearPMap.addBounded_domain {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : (addBounded A V).domain = A.domain

A bounded perturbation leaves the domain unchanged — V is everywhere defined, so A + V is defined exactly where A is. This is what makes perturbation arguments comparable on the nose rather than up to a domain inclusion.

@[simp]

theorem TauCeti.LinearPMap.addBounded_apply {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) (x : ↥(addBounded A V).domain) : ↑(addBounded A V) x = ↑A x + V ↑x

The perturbed map acts by A x + V x.

@[simp]

theorem TauCeti.LinearPMap.addBounded_neg_cancel {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : addBounded (addBounded A V) (-V) = A

A bounded perturbation is undone by its negation, on the nose.

addBounded leaves the domain alone, so (A + V) + (-V) is A as a partial map rather than merely an extension of it. This is what lets a theorem stated with the roles of the unperturbed and perturbed operators exchanged be applied without any domain bookkeeping.

def TauCeti.LinearPMap.LeftShiftedInverseBound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c s : ℝ) : Prop

A bounded left inverse for the real shift of a partial map.

Equations

• TauCeti.LinearPMap.LeftShiftedInverseBound A c s = ∃ (J : E →L[𝕜] E), (∀ (x : ↥A.domain), J (↑A x - ↑c • ↑x) = ↑x) ∧ ‖J‖ ≤ s⁻¹

def TauCeti.LinearPMap.TwoSidedShiftedInverseBound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c s : ℝ) : Prop

A bounded two-sided inverse for the real shift of a partial map, with the domain transport required by the right-inverse leg.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LinearPMap.TwoSidedShiftedInverseBound.leftShiftedInverseBound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {c s : ℝ} (h : TwoSidedShiftedInverseBound A c s) : LeftShiftedInverseBound A c s

A two-sided shifted inverse supplies its left-inverse component.

def TauCeti.LinearPMap.RelativelyBounded {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : ↥A.domain →ₗ[𝕜] E) (a b : ℝ) : Prop

Relative boundedness of a domain-defined perturbation with respect to a partial linear map.

Equations

• TauCeti.LinearPMap.RelativelyBounded A V a b = ∀ (x : ↥A.domain), ‖V x‖ ≤ a * ‖↑x‖ + b * ‖↑A x‖

theorem TauCeti.LinearPMap.RelativelyBounded.zero {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : RelativelyBounded A 0 0 0

The zero perturbation has zero relative bound.

theorem TauCeti.LinearPMap.RelativelyBounded.mono {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {V : ↥A.domain →ₗ[𝕜] E} {a b a' b' : ℝ} (hV : RelativelyBounded A V a b) (haa' : a ≤ a') (hbb' : b ≤ b') : RelativelyBounded A V a' b'

Relative bounds may be weakened by increasing either coefficient.

theorem TauCeti.LinearPMap.RelativelyBounded.add {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {V W : ↥A.domain →ₗ[𝕜] E} {a b c d : ℝ} (hV : RelativelyBounded A V a b) (hW : RelativelyBounded A W c d) : RelativelyBounded A (V + W) (a + c) (b + d)

Relative bounds add under addition of perturbations.

theorem TauCeti.LinearPMap.RelativelyBounded.smul {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {V : ↥A.domain →ₗ[𝕜] E} {a b : ℝ} (hV : RelativelyBounded A V a b) (c : 𝕜) : RelativelyBounded A (c • V) (‖c‖ * a) (‖c‖ * b)

Relative bounds scale by the norm of the scalar.

theorem TauCeti.LinearPMap.RelativelyBounded.neg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {V : ↥A.domain →ₗ[𝕜] E} {a b : ℝ} (hV : RelativelyBounded A V a b) : RelativelyBounded A (-V) a b

Relative bounds are preserved by negation.

theorem TauCeti.LinearPMap.RelativelyBounded.sub {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {V W : ↥A.domain →ₗ[𝕜] E} {a b c d : ℝ} (hV : RelativelyBounded A V a b) (hW : RelativelyBounded A W c d) : RelativelyBounded A (V - W) (a + c) (b + d)

Relative bounds add under subtraction of perturbations.

theorem TauCeti.LinearPMap.RelativelyBounded.domRestrict {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : RelativelyBounded A ((↑V).domRestrict A.domain) ‖V‖ 0

Restricting a bounded ambient operator to the domain gives relative bound (‖V‖, 0).

def TauCeti.LinearPMap.realResolventSet {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Set ℝ

Real resolvent set of a partial linear map. A parameter belongs to the set when the shifted map has a bounded two-sided inverse with explicit domain transport for the right-inverse leg.

Equations

• TauCeti.LinearPMap.realResolventSet A = {lam : ℝ | ∃ (R : E →L[𝕜] E), (∀ (x : ↥A.domain), R (↑A x - ↑lam • ↑x) = ↑x) ∧ ∀ (y : E), ∃ (h : R y ∈ A.domain), ↑A ⟨R y, h⟩ - ↑lam • R y = y}

theorem TauCeti.LinearPMap.mem_realResolventSet_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {lam : ℝ} : lam ∈ realResolventSet A ↔ ∃ (R : E →L[𝕜] E), (∀ (x : ↥A.domain), R (↑A x - ↑lam • ↑x) = ↑x) ∧ ∀ (y : E), ∃ (h : R y ∈ A.domain), ↑A ⟨R y, h⟩ - ↑lam • R y = y

Unfolds real resolvent membership through a stable public API.

realResolventSet is intentionally kept abstract across module boundaries; downstream proofs should use this theorem instead of depending on definitional transparency.

def TauCeti.LinearPMap.realSpectrum {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Set ℝ

Real spectrum defined as the complement of realResolventSet.

Equations

• TauCeti.LinearPMap.realSpectrum A = (TauCeti.LinearPMap.realResolventSet A)ᶜ

@[simp]

theorem TauCeti.LinearPMap.mem_realSpectrum_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {lam : ℝ} : lam ∈ realSpectrum A ↔ lam ∉ realResolventSet A

A real scalar is spectral exactly when it is not a real resolvent point.

theorem TauCeti.LinearPMap.mem_realSpectrum_of_eigenvector {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {lam : ℝ} {x : ↥A.domain} (hx : ↑x ≠ 0) (heig : ↑A x = ↑lam • ↑x) : lam ∈ realSpectrum A

A real eigenvalue is a real spectral point. A left inverse of the shifted map would have to send 0 back to the eigenvector, so no such bounded inverse exists.

This is the introduction rule for realSpectrum: every other lemma about it either consumes membership or proves a containment, and a containment is vacuously true of an operator with no spectrum at all. Only the surjectivity half of realResolventSet is unused here, so the hypotheses are the weakest possible — no closedness, no dense domain, and no symmetry.

def TauCeti.LinearPMap.SpectralSetsSeparated {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (s t : Set ℝ) (d : ℝ) : Prop

Spectral-set separation for two partial maps, possibly on different Hilbert spaces.

Equations

• TauCeti.LinearPMap.SpectralSetsSeparated A B s t d = ∀ a ∈ TauCeti.LinearPMap.realSpectrum A, a ∈ s → ∀ b ∈ TauCeti.LinearPMap.realSpectrum B, b ∈ t → d ≤ |a - b|

theorem TauCeti.LinearPMap.SpectralSetsSeparated.symm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {s t : Set ℝ} {d : ℝ} (h : SpectralSetsSeparated A B s t d) : SpectralSetsSeparated B A t s d

Spectral-set separation is symmetric in the two maps.

theorem TauCeti.LinearPMap.SpectralSetsSeparated.mono_gap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {s t : Set ℝ} {d e : ℝ} (h : SpectralSetsSeparated A B s t d) (hed : e ≤ d) : SpectralSetsSeparated A B s t e

Weakening the required gap preserves spectral-set separation.

theorem TauCeti.LinearPMap.SpectralSetsSeparated.mono_sets {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {s s' t t' : Set ℝ} {d : ℝ} (h : SpectralSetsSeparated A B s t d) (hs : s' ⊆ s) (ht : t' ⊆ t) : SpectralSetsSeparated A B s' t' d

Restricting either selected spectral set preserves separation.