Sylvester equations for partial linear maps

The domain-aware equation A X - X B = C, semibounds, and bounded-everywhere inverse data stated directly for Mathlib LinearPMap operators. Analytic properties such as closedness, dense domain, and self-adjointness remain separate hypotheses for the theorems that require them.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/Sylvester/ClosedSylvesterEquation.lean.
• Extraction class: representation migration and generalization from the bundled DKPS PartialMap to raw Mathlib LinearPMap.
• Spectra influence: none. This module depends only on Mathlib and the dependency-clean LinearPMap domain API.

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

Lower semibound for a partial linear map.

Equations

• TauCeti.LinearPMap.SemiboundedBelow A c = ∀ (x : ↥A.domain), c * ‖↑x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (↑A x) ↑x)

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

Upper semibound for a partial linear map.

Equations

• TauCeti.LinearPMap.SemiboundedAbove A c = ∀ (x : ↥A.domain), RCLike.re (inner 𝕜 (↑A x) ↑x) ≤ c * ‖↑x‖ ^ 2

theorem TauCeti.LinearPMap.semiboundedBelow_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : SemiboundedBelow A c ↔ ∀ (x : ↥A.domain), c * ‖↑x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (↑A x) ↑x)

Unfolds the lower semibound through a stable public API: SemiboundedBelow is kept abstract across module boundaries, so consumers use this rather than definitional transparency.

theorem TauCeti.LinearPMap.semiboundedAbove_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : SemiboundedAbove A c ↔ ∀ (x : ↥A.domain), RCLike.re (inner 𝕜 (↑A x) ↑x) ≤ c * ‖↑x‖ ^ 2

Unfolds the upper semibound through a stable public API.

theorem TauCeti.LinearPMap.SemiboundedBelow.mono {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {c d : ℝ} (hA : SemiboundedBelow A c) (hdc : d ≤ c) : SemiboundedBelow A d

A lower semibound remains valid after decreasing the constant.

theorem TauCeti.LinearPMap.SemiboundedAbove.mono {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {c d : ℝ} (hA : SemiboundedAbove A c) (hcd : c ≤ d) : SemiboundedAbove A d

An upper semibound remains valid after increasing the constant.

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

Domain-aware Sylvester equation A X - X B = C for partial linear maps.

• mapsTo_domain : MapsDomainTo A B X
• equation (x : ↥B.domain) : ↑A ⟨X ↑x, ⋯⟩ - X (↑B x) = C ↑x

theorem TauCeti.LinearPMap.SylvesterEquation.mapsTo {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {X C : F →L[𝕜] E} (h : SylvesterEquation A B X C) : MapsDomainTo A B X

Extract domain transport from a Sylvester equation.

theorem TauCeti.LinearPMap.SylvesterEquation.ofBounded {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {X C : F →L[𝕜] E} (hEq : A ∘SL X - X ∘SL B = C) : SylvesterEquation ((↑A).toPMap ⊤) ((↑B).toPMap ⊤) X C

A bounded Sylvester equation is a full-domain partial-map equation.

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

The zero map solves the homogeneous domain-aware equation.

theorem TauCeti.LinearPMap.SylvesterEquation.add {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {X Y C D : F →L[𝕜] E} (hX : SylvesterEquation A B X C) (hY : SylvesterEquation A B Y D) : SylvesterEquation A B (X + Y) (C + D)

Domain-aware Sylvester equations add.

theorem TauCeti.LinearPMap.SylvesterEquation.neg {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {X C : F →L[𝕜] E} (hX : SylvesterEquation A B X C) : SylvesterEquation A B (-X) (-C)

Domain-aware Sylvester equations are preserved by negation.

theorem TauCeti.LinearPMap.SylvesterEquation.sub {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {X Y C D : F →L[𝕜] E} (hX : SylvesterEquation A B X C) (hY : SylvesterEquation A B Y D) : SylvesterEquation A B (X - Y) (C - D)

Domain-aware Sylvester equations subtract.

theorem TauCeti.LinearPMap.SylvesterEquation.smul {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {X C : F →L[𝕜] E} (hX : SylvesterEquation A B X C) (c : 𝕜) : SylvesterEquation A B (c • X) (c • C)

Domain-aware Sylvester equations commute with scalar multiplication.

@[reducible, inline]

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

A Sylvester equation with a partial left block and a bounded right block. This is the ordinary partial-map equation with the right block embedded on its full domain.

Equations

• TauCeti.LinearPMap.UnboundedBoundedSylvesterEquation A B X C = TauCeti.LinearPMap.SylvesterEquation A ((↑B).toPMap ⊤) X C

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

A partial linear map whose inverse is everywhere defined and bounded.

• inv : E →L[𝕜] E

  The bounded everywhere-defined inverse, whose range lies in the partial operator's domain.

• inv_mapsTo_domain (y : E) : self.inv y ∈ A.domain
• apply_inv (y : E) : ↑A ⟨self.inv y, ⋯⟩ = y
• inv_apply (x : ↥A.domain) : self.inv (↑A x) = ↑x

theorem TauCeti.LinearPMap.HasBoundedEverywhereInverse.injective {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} (hA : HasBoundedEverywhereInverse A) : Function.Injective ↑A

A partial map with an everywhere-defined two-sided inverse is injective.

theorem TauCeti.LinearPMap.HasBoundedEverywhereInverse.surjective {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} (hA : HasBoundedEverywhereInverse A) : Function.Surjective ↑A

A partial map with an everywhere-defined two-sided inverse is surjective onto the ambient codomain.