# Compact operators #

In this file we define compact linear operators between two topological vector spaces (TVS).

## Main definitions #

• IsCompactOperator : predicate for compact operators

## Main statements #

• isCompactOperator_iff_isCompact_closure_image_ball : the usual characterization of compact operators from a normed space to a T2 TVS.
• IsCompactOperator.comp_clm : precomposing a compact operator by a continuous linear map gives a compact operator
• IsCompactOperator.clm_comp : postcomposing a compact operator by a continuous linear map gives a compact operator
• IsCompactOperator.continuous : compact operators are automatically continuous
• isClosed_setOf_isCompactOperator : the set of compact operators is closed for the operator norm

## Implementation details #

We define IsCompactOperator as a predicate, because the space of compact operators inherits all of its structure from the space of continuous linear maps (e.g we want to have the usual operator norm on compact operators).

The two natural options then would be to make it a predicate over linear maps or continuous linear maps. Instead we define it as a predicate over bare functions, although it really only makes sense for linear functions, because Lean is really good at finding coercions to bare functions (whereas coercing from continuous linear maps to linear maps often needs type ascriptions).

## References #

• [N. Bourbaki, Théories Spectrales, Chapitre 3][bourbaki2023]

## Tags #

Compact operator

def IsCompactOperator {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [] [] (f : M₁M₂) :

A compact operator between two topological vector spaces. This definition is usually given as "there exists a neighborhood of zero whose image is contained in a compact set", but we choose a definition which involves fewer existential quantifiers and replaces images with preimages.

We prove the equivalence in isCompactOperator_iff_exists_mem_nhds_image_subset_compact.

Equations
Instances For
theorem isCompactOperator_zero {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [] [] [Zero M₂] :
theorem isCompactOperator_iff_exists_mem_nhds_image_subset_compact {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] (f : M₁M₂) :
∃ V ∈ nhds 0, ∃ (K : Set M₂), f '' V K
theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [T2Space M₂] (f : M₁M₂) :
∃ V ∈ nhds 0, IsCompact (closure (f '' V))
theorem IsCompactOperator.image_subset_compact_of_isVonNBounded {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) {S : Set M₁} (hS : ) :
∃ (K : Set M₂), f '' S K
theorem IsCompactOperator.isCompact_closure_image_of_isVonNBounded {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) {S : Set M₁} (hS : ) :
IsCompact (closure (f '' S))
theorem IsCompactOperator.image_subset_compact_of_bounded {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) {S : Set M₁} (hS : ) :
∃ (K : Set M₂), f '' S K
theorem IsCompactOperator.isCompact_closure_image_of_bounded {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) {S : Set M₁} (hS : ) :
IsCompact (closure (f '' S))
theorem IsCompactOperator.image_ball_subset_compact {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) (r : ) :
∃ (K : Set M₂), f '' K
theorem IsCompactOperator.image_closedBall_subset_compact {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) (r : ) :
∃ (K : Set M₂), f '' K
theorem IsCompactOperator.isCompact_closure_image_ball {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) (r : ) :
IsCompact (closure (f '' ))
theorem IsCompactOperator.isCompact_closure_image_closedBall {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) (r : ) :
IsCompact (closure (f '' ))
theorem isCompactOperator_iff_image_ball_subset_compact {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : } (hr : 0 < r) :
∃ (K : Set M₂), f '' K
theorem isCompactOperator_iff_image_closedBall_subset_compact {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : } (hr : 0 < r) :
∃ (K : Set M₂), f '' K
theorem isCompactOperator_iff_isCompact_closure_image_ball {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : } (hr : 0 < r) :
IsCompact (closure (f '' ))
theorem isCompactOperator_iff_isCompact_closure_image_closedBall {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [T2Space M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) {r : } (hr : 0 < r) :
IsCompact (closure (f '' ))
theorem IsCompactOperator.smul {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [] {S : Type u_9} [] [] [] {f : M₁M₂} (hf : ) (c : S) :
theorem IsCompactOperator.add {M₁ : Type u_5} {M₂ : Type u_6} [] [] [] [] [] {f : M₁M₂} {g : M₁M₂} (hf : ) (hg : ) :
theorem IsCompactOperator.neg {M₁ : Type u_5} {M₄ : Type u_8} [] [] [] [] [] {f : M₁M₄} (hf : ) :
theorem IsCompactOperator.sub {M₁ : Type u_5} {M₄ : Type u_8} [] [] [] [] [] {f : M₁M₄} {g : M₁M₄} (hf : ) (hg : ) :
def compactOperator {R₁ : Type u_1} {R₄ : Type u_4} [Semiring R₁] [] (σ₁₄ : R₁ →+* R₄) (M₁ : Type u_5) (M₄ : Type u_8) [] [] [] [] [Module R₁ M₁] [Module R₄ M₄] [] [] :
Submodule R₄ (M₁ →SL[σ₁₄] M₄)

The submodule of compact continuous linear maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsCompactOperator.comp_clm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] [Module R₁ M₁] [] [Module R₂ M₂] {f : M₂M₃} (hf : ) (g : M₁ →SL[σ₁₂] M₂) :
theorem IsCompactOperator.continuous_comp {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] {f : M₁M₂} (hf : ) {g : M₂M₃} (hg : ) :
theorem IsCompactOperator.clm_comp {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₂] [Semiring R₃] {σ₂₃ : R₂ →+* R₃} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] [] [Module R₂ M₂] [] [Module R₃ M₃] {f : M₁M₂} (hf : ) (g : M₂ →SL[σ₂₃] M₃) :
theorem IsCompactOperator.codRestrict {R₂ : Type u_2} [Semiring R₂] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module R₂ M₂] {f : M₁M₂} (hf : ) {V : Submodule R₂ M₂} (hV : ∀ (x : M₁), f x V) (h_closed : IsClosed V) :
theorem IsCompactOperator.restrict {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [] [] [Module R₁ M₁] {f : M₁ →ₗ[R₁] M₁} (hf : ) {V : Submodule R₁ M₁} (hV : vV, f v V) (h_closed : IsClosed V) :

If a compact operator preserves a closed submodule, its restriction to that submodule is compact.

Note that, following mathlib's convention in linear algebra, restrict designates the restriction of an endomorphism f : E →ₗ E to an endomorphism f' : ↥V →ₗ ↥V. To prove that the restriction f' : ↥U →ₛₗ ↥V of a compact operator f : E →ₛₗ F is compact, apply IsCompactOperator.codRestrict to f ∘ U.subtypeL, which is compact by IsCompactOperator.comp_clm.

theorem IsCompactOperator.restrict' {R₂ : Type u_2} [Semiring R₂] {M₂ : Type u_5} [] [] [Module R₂ M₂] [T0Space M₂] {f : M₂ →ₗ[R₂] M₂} (hf : ) {V : Submodule R₂ M₂} (hV : vV, f v V) [hcomplete : ] :

If a compact operator preserves a complete submodule, its restriction to that submodule is compact.

Note that, following mathlib's convention in linear algebra, restrict designates the restriction of an endomorphism f : E →ₗ E to an endomorphism f' : ↥V →ₗ ↥V. To prove that the restriction f' : ↥U →ₛₗ ↥V of a compact operator f : E →ₛₗ F is compact, apply IsCompactOperator.codRestrict to f ∘ U.subtypeL, which is compact by IsCompactOperator.comp_clm.

theorem IsCompactOperator.continuous {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ₁₂ : 𝕜₁ →+* 𝕜₂} [] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
def ContinuousLinearMap.mkOfIsCompactOperator {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ₁₂ : 𝕜₁ →+* 𝕜₂} [] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
M₁ →SL[σ₁₂] M₂

Upgrade a compact LinearMap to a ContinuousLinearMap.

Equations
• = { toLinearMap := f, cont := }
Instances For
@[simp]
theorem ContinuousLinearMap.mkOfIsCompactOperator_to_linearMap {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ₁₂ : 𝕜₁ →+* 𝕜₂} [] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
@[simp]
theorem ContinuousLinearMap.coe_mkOfIsCompactOperator {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ₁₂ : 𝕜₁ →+* 𝕜₂} [] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
theorem ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {σ₁₂ : 𝕜₁ →+* 𝕜₂} [] {M₁ : Type u_3} {M₂ : Type u_4} [] [] [] [] [Module 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : ) :
theorem isClosed_setOf_isCompactOperator {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [T2Space M₂] [] :
IsClosed {f : M₁ →SL[σ₁₂] M₂ | }

The set of compact operators from a normed space to a complete topological vector space is closed.

theorem compactOperator_topologicalClosure {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_3} {M₂ : Type u_4} [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [T2Space M₂] [] :
Submodule.topologicalClosure (compactOperator σ₁₂ M₁ M₂) = compactOperator σ₁₂ M₁ M₂
theorem isCompactOperator_of_tendsto {ι : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_4} {M₂ : Type u_5} [] [NormedSpace 𝕜₁ M₁] [Module 𝕜₂ M₂] [] [] [] [T2Space M₂] [] {l : } [] {F : ιM₁ →SL[σ₁₂] M₂} {f : M₁ →SL[σ₁₂] M₂} (hf : Filter.Tendsto F l (nhds f)) (hF : ∀ᶠ (i : ι) in l, IsCompactOperator (F i)) :