Documentation

TauCeti.Analysis.OperatorIdeal.Carrier

Operator gauges and their normed carriers #

An operator gauge g : OperatorGauge 𝕜 E F assigns an extended value g A ∈ [0, ∞] to every bounded operator A : E →L[𝕜] F between normed spaces. It is subadditive, absolutely homogeneous, and dominates the operator norm. Examples are the Schatten and Ky Fan gauges on Hilbert spaces, and the nuclear and absolutely summing gauges on Banach spaces; the operator-ideal families of TauCeti.Analysis.OperatorIdeal.Family restrict to operator gauges on each pair of Hilbert spaces.

The operators of finite gauge form the submodule g.finiteSubmodule of E →L[𝕜] F. The finite real value of the gauge is a norm on it, in general finer than the operator norm. Since that norm differs from the operator norm, the finite-gauge operators are packaged as a separate type g.Carrier rather than as the subtype of g.finiteSubmodule, which would inherit the operator norm.

When F is a normed space, the carrier g.Carrier is a normed space over 𝕜 with ‖T‖ = (g T).toReal. No information is lost in passing to the real norm, since ‖T‖ₑ = g T, and the inclusion into bounded operators is a contraction. If moreover F is complete and the gauge is lower semicontinuous for the operator-norm topology, then the carrier is a Banach space: a Cauchy sequence for the gauge norm is Cauchy for the operator norm, and lower semicontinuity bounds the gauge of the distance to its operator-norm limit.

Main declarations #

TauCeti.OperatorGauge: an extended gauge on bounded operators.
TauCeti.OperatorGauge.finiteSubmodule: the submodule of operators of finite gauge.
TauCeti.OperatorGauge.Carrier: the normed space of operators of finite gauge.
TauCeti.OperatorGauge.Carrier.norm_def, TauCeti.OperatorGauge.Carrier.enorm_eq_gauge: the norm of the carrier is the gauge.
TauCeti.OperatorGauge.Carrier.toContinuousLinearMapL: the contractive inclusion of the carrier into bounded operators.
TauCeti.OperatorGauge.completeSpace_carrier_of_lowerSemicontinuous: a lower semicontinuous gauge into a Banach space has a complete carrier.

References #

A. Pietsch, Operator Ideals, North-Holland, 1980, Chapter 6.
B. Simon, Trace Ideals and Their Applications, second edition, AMS, 2005, Chapter 2.

structure TauCeti.OperatorGauge (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

Type (max u_2 u_3)

An operator gauge on E →L[𝕜] F: an extended nonnegative function on bounded operators that is subadditive, absolutely homogeneous and dominates the operator norm.

toFun : (E →L[𝕜] F) → ENNReal
The gauge of a bounded operator.
map_add_le' (A B : E →L[𝕜] F) : self.toFun (A + B) ≤ self.toFun A + self.toFun B
The gauge is subadditive.
map_smul' (c : 𝕜) (A : E →L[𝕜] F) : self.toFun (c • A) = ‖c‖ₑ * self.toFun A
The gauge is absolutely homogeneous.
enorm_le' (A : E →L[𝕜] F) : ‖A‖ₑ ≤ self.toFun A
The gauge dominates the extended operator norm.

Instances For

@[instance_reducible]

instance TauCeti.OperatorGauge.instFunLikeContinuousLinearMapIdENNReal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :

FunLike (OperatorGauge 𝕜 E F) (E →L[𝕜] F) ENNReal

theorem TauCeti.OperatorGauge.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g h : OperatorGauge 𝕜 E F} (H : ∀ (A : E →L[𝕜] F), g A = h A) :

g = h

theorem TauCeti.OperatorGauge.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g h : OperatorGauge 𝕜 E F} :

g = h ↔ ∀ (A : E →L[𝕜] F), g A = h A

@[simp]

theorem TauCeti.OperatorGauge.coe_mk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : (E →L[𝕜] F) → ENNReal) (h₁ : ∀ (A B : E →L[𝕜] F), f (A + B) ≤ f A + f B) (h₂ : ∀ (c : 𝕜) (A : E →L[𝕜] F), f (c • A) = ‖c‖ₑ * f A) (h₃ : ∀ (A : E →L[𝕜] F), ‖A‖ₑ ≤ f A) :

⇑{ toFun := f, map_add_le' := h₁, map_smul' := h₂, enorm_le' := h₃ } = f

@[simp]

theorem TauCeti.OperatorGauge.toFun_eq_coe {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

g.toFun = ⇑g

theorem TauCeti.OperatorGauge.map_add_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) (A B : E →L[𝕜] F) :

g (A + B) ≤ g A + g B

An operator gauge is subadditive.

@[simp]

theorem TauCeti.OperatorGauge.map_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) (c : 𝕜) (A : E →L[𝕜] F) :

g (c • A) = ‖c‖ₑ * g A

An operator gauge is absolutely homogeneous.

theorem TauCeti.OperatorGauge.enorm_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) (A : E →L[𝕜] F) :

‖A‖ₑ ≤ g A

An operator gauge dominates the extended operator norm.

@[simp]

theorem TauCeti.OperatorGauge.map_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

g 0 = 0

@[simp]

theorem TauCeti.OperatorGauge.map_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) (A : E →L[𝕜] F) :

g (-A) = g A

@[simp]

theorem TauCeti.OperatorGauge.map_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) {A : E →L[𝕜] F} :

g A = 0 ↔ A = 0

An operator gauge into a normed space vanishes exactly at zero.

The submodule of operators of finite gauge #

def TauCeti.OperatorGauge.finiteSubmodule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

Submodule 𝕜 (E →L[𝕜] F)

The operators of finite gauge form a submodule of the bounded operators.

Instances For

@[simp]

theorem TauCeti.OperatorGauge.mem_finiteSubmodule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} {A : E →L[𝕜] F} :

A ∈ g.finiteSubmodule ↔ g A < ⊤

The normed carrier #

structure TauCeti.OperatorGauge.Carrier {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

Type (max u_2 u_3)

The operators of finite gauge, normed by the finite real value of the gauge.

This is a separate type from the subtype of g.finiteSubmodule, which carries the operator norm.

toContinuousLinearMap : E →L[𝕜] F
The underlying bounded operator.
mem_finiteSubmodule : self.toContinuousLinearMap ∈ g.finiteSubmodule
The underlying operator has finite gauge.

Instances For

theorem TauCeti.OperatorGauge.Carrier.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {inst✝ : NontriviallyNormedField 𝕜} {inst✝¹ : SeminormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {inst✝³ : SeminormedAddCommGroup F} {inst✝⁴ : NormedSpace 𝕜 F} {g : OperatorGauge 𝕜 E F} {x y : g.Carrier} (toContinuousLinearMap : x.toContinuousLinearMap = y.toContinuousLinearMap) :

x = y

theorem TauCeti.OperatorGauge.Carrier.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {inst✝ : NontriviallyNormedField 𝕜} {inst✝¹ : SeminormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {inst✝³ : SeminormedAddCommGroup F} {inst✝⁴ : NormedSpace 𝕜 F} {g : OperatorGauge 𝕜 E F} {x y : g.Carrier} :

x = y ↔ x.toContinuousLinearMap = y.toContinuousLinearMap

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

Function.Injective toContinuousLinearMap

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_inj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} {S T : g.Carrier} :

S.toContinuousLinearMap = T.toContinuousLinearMap ↔ S = T

@[simp]

theorem TauCeti.OperatorGauge.Carrier.range_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

Set.range toContinuousLinearMap = ↑g.finiteSubmodule

The underlying operators of the carrier are exactly the operators of finite gauge.

theorem TauCeti.OperatorGauge.Carrier.gauge_lt_top {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

g T.toContinuousLinearMap < ⊤

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instZero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instAdd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instNeg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instSub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instSMulOfIsScalarTowerContinuousLinearMapId {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} {R : Type u_4} [SMul R 𝕜] [SMul R (E →L[𝕜] F)] [IsScalarTower R 𝕜 (E →L[𝕜] F)] :

SMul R g.Carrier

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

toContinuousLinearMap 0 = 0

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (S T : g.Carrier) :

(S + T).toContinuousLinearMap = S.toContinuousLinearMap + T.toContinuousLinearMap

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

(-T).toContinuousLinearMap = -T.toContinuousLinearMap

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (S T : g.Carrier) :

(S - T).toContinuousLinearMap = S.toContinuousLinearMap - T.toContinuousLinearMap

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMap_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} {R : Type u_4} [SMul R 𝕜] [SMul R (E →L[𝕜] F)] [IsScalarTower R 𝕜 (E →L[𝕜] F)] (c : R) (T : g.Carrier) :

(c • T).toContinuousLinearMap = c • T.toContinuousLinearMap

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

AddCommGroup g.Carrier

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instModule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

Module 𝕜 g.Carrier

def TauCeti.OperatorGauge.Carrier.addGroupNorm {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

AddGroupNorm g.Carrier

The gauge of the underlying operator, as an additive group norm on the carrier.

Instances For

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instNormedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

NormedAddCommGroup g.Carrier

theorem TauCeti.OperatorGauge.Carrier.norm_def {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

‖T‖ = (g T.toContinuousLinearMap).toReal

The norm of an element of the carrier is the finite real value of its gauge.

@[simp]

theorem TauCeti.OperatorGauge.Carrier.enorm_eq_gauge {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

‖T‖ₑ = g T.toContinuousLinearMap

The extended norm of an element of the carrier is its gauge.

theorem TauCeti.OperatorGauge.Carrier.ofReal_norm_eq_gauge {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

ENNReal.ofReal ‖T‖ = g T.toContinuousLinearMap

Passing from the gauge to the real norm of the carrier loses no information.

@[instance_reducible]

instance TauCeti.OperatorGauge.Carrier.instNormedSpace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

NormedSpace 𝕜 g.Carrier

theorem TauCeti.OperatorGauge.Carrier.norm_toContinuousLinearMap_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

‖T.toContinuousLinearMap‖ ≤ ‖T‖

The operator norm is dominated by the norm of the carrier.

noncomputable def TauCeti.OperatorGauge.Carrier.toContinuousLinearMapL {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : OperatorGauge 𝕜 E F) :

g.Carrier →L[𝕜] E →L[𝕜] F

The inclusion of the carrier into the bounded operators, as a bounded linear map.

Instances For

@[simp]

theorem TauCeti.OperatorGauge.Carrier.toContinuousLinearMapL_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} (T : g.Carrier) :

(toContinuousLinearMapL g) T = T.toContinuousLinearMap

theorem TauCeti.OperatorGauge.Carrier.norm_toContinuousLinearMapL_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} :

‖toContinuousLinearMapL g‖ ≤ 1

The inclusion of the carrier into the bounded operators is a contraction.

Completeness #

theorem TauCeti.OperatorGauge.completeSpace_carrier_of_lowerSemicontinuous {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : OperatorGauge 𝕜 E F} [CompleteSpace F] (h : LowerSemicontinuous ⇑g) :

CompleteSpace g.Carrier

If the target is complete and the gauge is lower semicontinuous for the operator-norm topology, then the carrier is complete.