Weakly compact operators

A bounded operator T : E →L[𝕜] F between real or complex normed spaces is weakly compact if the image of the closed unit ball of E is relatively compact in the weak topology of F, that is, its closure in WeakSpace 𝕜 F is compact. Equivalently, T is a compact operator into WeakSpace 𝕜 F; this lets weak compactness reuse Mathlib's IsCompactOperator API.

Main results

• ContinuousLinearMap.isWeaklyCompact_iff_isCompactOperator: weak compactness as compactness into the weak topology.
• ContinuousLinearMap.IsWeaklyCompact.add, .smul, .comp_clm, .clm_comp: weakly compact operators are stable under sums, scalar multiples and composition with bounded operators.
• IsCompactOperator.isWeaklyCompact: compact operators are weakly compact.
• ContinuousLinearMap.isWeaklyCompact_id_iff: the identity is weakly compact exactly on a reflexive space; on an infinite-dimensional reflexive space it is weakly compact but not compact.
• ContinuousLinearMap.isWeaklyCompact_iff_range_subset: Gantmacher's criterion, T is weakly compact iff its bidual adjoint T** takes values in the canonical image of F.
• ContinuousLinearMap.isWeaklyCompact_precomp_iff: Gantmacher's theorem, an operator into a Banach space is weakly compact iff its adjoint is.

The adjoint of T is ContinuousLinearMap.precomp 𝕜 T, and the bidual adjoint is obtained by applying precomp twice.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §3.5.

def ContinuousLinearMap.IsWeaklyCompact {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) : Prop

A bounded operator is weakly compact if the image of the closed unit ball is relatively compact in the weak topology of the codomain: its closure in WeakSpace 𝕜 F is compact.

theorem ContinuousLinearMap.isWeaklyCompact_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T.IsWeaklyCompact ↔ IsCompact (closure (⇑(toWeakSpace 𝕜 F) '' ⇑T '' Metric.closedBall 0 1))

Unfolding lemma for ContinuousLinearMap.IsWeaklyCompact.

theorem ContinuousLinearMap.isWeaklyCompact_iff_isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T.IsWeaklyCompact ↔ IsCompactOperator (⇑(toWeakSpace 𝕜 F) ∘ ⇑T)

A bounded operator is weakly compact iff, as a map into the weak topology of its codomain, it is a compact operator.

theorem ContinuousLinearMap.IsWeaklyCompact.of_isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : IsCompactOperator (⇑(toWeakSpace 𝕜 F) ∘ ⇑T) → T.IsWeaklyCompact

Alias of the reverse direction of ContinuousLinearMap.isWeaklyCompact_iff_isCompactOperator.

---

A bounded operator is weakly compact iff, as a map into the weak topology of its codomain, it is a compact operator.

theorem ContinuousLinearMap.IsWeaklyCompact.isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T.IsWeaklyCompact → IsCompactOperator (⇑(toWeakSpace 𝕜 F) ∘ ⇑T)

Alias of the forward direction of ContinuousLinearMap.isWeaklyCompact_iff_isCompactOperator.

---

A bounded operator is weakly compact iff, as a map into the weak topology of its codomain, it is a compact operator.

theorem ContinuousLinearMap.IsWeaklyCompact.isCompact_closure_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) {s : Set E} (hs : Bornology.IsBounded s) : IsCompact (closure (⇑(toWeakSpace 𝕜 F) '' ⇑T '' s))

A weakly compact operator maps every bounded set to a relatively weakly compact set.

theorem ContinuousLinearMap.isWeaklyCompact_iff_exists_isCompact {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T.IsWeaklyCompact ↔ ∃ (K : Set (WeakSpace 𝕜 F)), IsCompact K ∧ ⇑(toWeakSpace 𝕜 F) '' ⇑T '' Metric.closedBall 0 1 ⊆ K

A bounded operator is weakly compact iff the image of the unit ball lies in a weakly compact set.

Algebraic operations

@[simp]

theorem ContinuousLinearMap.isWeaklyCompact_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : IsWeaklyCompact 0

The zero operator is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T S : E →L[𝕜] F} (hT : T.IsWeaklyCompact) (hS : S.IsWeaklyCompact) : (T + S).IsWeaklyCompact

The sum of two weakly compact operators is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) (c : 𝕜) : (c • T).IsWeaklyCompact

A scalar multiple of a weakly compact operator is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) : (-T).IsWeaklyCompact

The negative of a weakly compact operator is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T S : E →L[𝕜] F} (hT : T.IsWeaklyCompact) (hS : S.IsWeaklyCompact) : (T - S).IsWeaklyCompact

The difference of two weakly compact operators is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.comp_clm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D : Type u_5} [SeminormedAddCommGroup D] [NormedSpace 𝕜 D] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) (S : D →L[𝕜] E) : (T ∘SL S).IsWeaklyCompact

Precomposing a weakly compact operator with a bounded operator gives a weakly compact operator.

theorem ContinuousLinearMap.IsWeaklyCompact.clm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) (S : F →L[𝕜] G) : (S ∘SL T).IsWeaklyCompact

Postcomposing a weakly compact operator with a bounded operator gives a weakly compact operator, since bounded operators are continuous for the weak topologies.

theorem IsCompactOperator.isWeaklyCompact {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : IsCompactOperator ⇑T) : T.IsWeaklyCompact

Every compact operator is weakly compact.

The identity operator

theorem ContinuousLinearMap.isWeaklyCompact_id_iff {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : (ContinuousLinearMap.id 𝕜 F).IsWeaklyCompact ↔ Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)

The identity of a normed space is weakly compact iff the space is reflexive.

theorem ContinuousLinearMap.isWeaklyCompact_id_and_not_isCompactOperator_id {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (hF : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)) (hdim : ¬FiniteDimensional 𝕜 F) : (ContinuousLinearMap.id 𝕜 F).IsWeaklyCompact ∧ ¬IsCompactOperator ⇑(ContinuousLinearMap.id 𝕜 F)

On an infinite-dimensional reflexive space, the identity is weakly compact but not compact. Thus weak compactness of operators is strictly weaker than compactness.

Gantmacher's theorem

theorem ContinuousLinearMap.IsWeaklyCompact.range_precomp_precomp_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) : Set.range ⇑(ContinuousLinearMap.precomp 𝕜 (ContinuousLinearMap.precomp 𝕜 T)) ⊆ Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)

Gantmacher's criterion, forward direction: the bidual adjoint T** of a weakly compact operator takes values in the canonical image of the codomain in its bidual.

theorem ContinuousLinearMap.IsWeaklyCompact.of_range_precomp_precomp_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (h : Set.range ⇑(ContinuousLinearMap.precomp 𝕜 (ContinuousLinearMap.precomp 𝕜 T)) ⊆ Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)) : T.IsWeaklyCompact

Gantmacher's criterion, reverse direction: a bounded operator whose bidual adjoint T** takes values in the canonical image of the codomain in its bidual is weakly compact.

theorem ContinuousLinearMap.isWeaklyCompact_iff_range_subset {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} : T.IsWeaklyCompact ↔ Set.range ⇑(precomp 𝕜 (precomp 𝕜 T)) ⊆ Set.range ⇑(NormedSpace.inclusionInDoubleDual 𝕜 F)

Gantmacher's criterion. A bounded operator is weakly compact iff its bidual adjoint T** takes values in the canonical image of the codomain in its bidual. No completeness is assumed.

theorem ContinuousLinearMap.IsWeaklyCompact.precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsWeaklyCompact) : (ContinuousLinearMap.precomp 𝕜 T).IsWeaklyCompact

Gantmacher's theorem, forward direction: the adjoint of a weakly compact operator is weakly compact.

theorem ContinuousLinearMap.IsWeaklyCompact.of_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} (hT : (ContinuousLinearMap.precomp 𝕜 T).IsWeaklyCompact) : T.IsWeaklyCompact

Gantmacher's theorem, reverse direction: an operator into a Banach space whose adjoint is weakly compact is weakly compact.

theorem ContinuousLinearMap.isWeaklyCompact_precomp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T : E →L[𝕜] F} : (precomp 𝕜 T).IsWeaklyCompact ↔ T.IsWeaklyCompact

Gantmacher's theorem. An operator into a Banach space is weakly compact iff its adjoint is weakly compact.