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 operatorIsCompactOperator.clm_comp: postcomposing a compact operator by a continuous linear map gives a compact operatorIsCompactOperator.continuous: compact operators are automatically continuousisClosed_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 #
Tags #
Compact operator
def
IsCompactOperator
{M₁ : Type u_1}
{M₂ : Type u_2}
[Zero M₁]
[TopologicalSpace M₁]
[TopologicalSpace 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.
Instances For
theorem
isCompactOperator_zero
{M₁ : Type u_1}
{M₂ : Type u_2}
[Zero M₁]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[Zero M₂]
:
theorem
isCompactOperator_iff_exists_mem_nhds_image_subset_compact
{M₁ : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
(f : M₁ → M₂)
:
theorem
isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image
{M₁ : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
[T2Space M₂]
(f : M₁ → M₂)
:
theorem
IsCompactOperator.image_subset_compact_of_isVonNBounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
{S : Set M₁}
(hS : Bornology.IsVonNBounded 𝕜₁ S)
:
theorem
IsCompactOperator.isCompact_closure_image_of_isVonNBounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
{S : Set M₁}
(hS : Bornology.IsVonNBounded 𝕜₁ S)
:
theorem
IsCompactOperator.image_subset_compact_of_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
{S : Set M₁}
(hS : Bornology.IsBounded S)
:
theorem
IsCompactOperator.isCompact_closure_image_of_bounded
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
{S : Set M₁}
(hS : Bornology.IsBounded S)
:
theorem
IsCompactOperator.image_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
(r : ℝ)
:
theorem
IsCompactOperator.image_closedBall_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
(r : ℝ)
:
theorem
IsCompactOperator.isCompact_closure_image_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
(r : ℝ)
:
IsCompact (closure (⇑f '' Metric.ball 0 r))
theorem
IsCompactOperator.isCompact_closure_image_closedBall
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
(r : ℝ)
:
IsCompact (closure (⇑f '' Metric.closedBall 0 r))
theorem
isCompactOperator_iff_image_ball_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r)
:
IsCompactOperator ⇑f ↔ ∃ (K : Set M₂), IsCompact K ∧ ⇑f '' Metric.ball 0 r ⊆ K
theorem
isCompactOperator_iff_image_closedBall_subset_compact
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r)
:
IsCompactOperator ⇑f ↔ ∃ (K : Set M₂), IsCompact K ∧ ⇑f '' Metric.closedBall 0 r ⊆ K
theorem
isCompactOperator_iff_isCompact_closure_image_ball
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r)
:
IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.ball 0 r))
theorem
isCompactOperator_iff_isCompact_closure_image_closedBall
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[SeminormedRing 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
(f : M₁ →ₛₗ[σ₁₂] M₂)
{r : ℝ}
(hr : 0 < r)
:
IsCompactOperator ⇑f ↔ IsCompact (closure (⇑f '' Metric.closedBall 0 r))
theorem
IsCompactOperator.smul
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{S : Type u_6}
[Monoid S]
[DistribMulAction S M₂]
[ContinuousConstSMul S M₂]
{f : M₁ → M₂}
(hf : IsCompactOperator f)
(c : S)
:
IsCompactOperator (c • f)
theorem
IsCompactOperator.add
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[ContinuousAdd M₂]
{f g : M₁ → M₂}
(hf : IsCompactOperator f)
(hg : IsCompactOperator g)
:
IsCompactOperator (f + g)
theorem
IsCompactOperator.neg
{M₁ : Type u_3}
{M₄ : Type u_5}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₄]
[AddCommGroup M₄]
[ContinuousNeg M₄]
{f : M₁ → M₄}
(hf : IsCompactOperator f)
:
theorem
IsCompactOperator.sub
{M₁ : Type u_3}
{M₄ : Type u_5}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₄]
[AddCommGroup M₄]
[TopologicalAddGroup M₄]
{f g : M₁ → M₄}
(hf : IsCompactOperator f)
(hg : IsCompactOperator g)
:
IsCompactOperator (f - g)
def
compactOperator
{R₁ : Type u_1}
{R₄ : Type u_2}
[Semiring R₁]
[CommSemiring R₄]
(σ₁₄ : R₁ →+* R₄)
(M₁ : Type u_3)
(M₄ : Type u_5)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[TopologicalSpace M₄]
[AddCommGroup M₄]
[Module R₁ M₁]
[Module R₄ M₄]
[ContinuousConstSMul R₄ M₄]
[TopologicalAddGroup M₄]
:
The submodule of compact continuous linear maps.
Equations
- compactOperator σ₁₄ M₁ M₄ = { carrier := {f : M₁ →SL[σ₁₄] M₄ | IsCompactOperator ⇑f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
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}
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
{f : M₂ → M₃}
(hf : IsCompactOperator f)
(g : M₁ →SL[σ₁₂] M₂)
:
IsCompactOperator (f ∘ ⇑g)
theorem
IsCompactOperator.continuous_comp
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[AddCommMonoid M₁]
{f : M₁ → M₂}
(hf : IsCompactOperator f)
{g : M₂ → M₃}
(hg : Continuous g)
:
IsCompactOperator (g ∘ f)
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}
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
[AddCommMonoid M₃]
[Module R₃ M₃]
{f : M₁ → M₂}
(hf : IsCompactOperator f)
(g : M₂ →SL[σ₂₃] M₃)
:
IsCompactOperator (⇑g ∘ f)
theorem
IsCompactOperator.codRestrict
{R₂ : Type u_1}
[Semiring R₂]
{M₁ : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
{f : M₁ → M₂}
(hf : IsCompactOperator f)
{V : Submodule R₂ M₂}
(hV : ∀ (x : M₁), f x ∈ V)
(h_closed : IsClosed ↑V)
:
IsCompactOperator (Set.codRestrict f (↑V) hV)
theorem
IsCompactOperator.restrict
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_3}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{f : M₁ →ₗ[R₁] M₁}
(hf : IsCompactOperator ⇑f)
{V : Submodule R₁ M₁}
(hV : ∀ v ∈ V, f v ∈ V)
(h_closed : IsClosed ↑V)
:
IsCompactOperator ⇑(f.restrict hV)
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_4}
[UniformSpace M₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
[T0Space M₂]
{f : M₂ →ₗ[R₂] M₂}
(hf : IsCompactOperator ⇑f)
{V : Submodule R₂ M₂}
(hV : ∀ v ∈ V, f v ∈ V)
[hcomplete : CompleteSpace ↥V]
:
IsCompactOperator ⇑(f.restrict hV)
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}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[TopologicalAddGroup M₁]
[ContinuousConstSMul 𝕜₁ M₁]
[TopologicalAddGroup M₂]
[ContinuousSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
:
Continuous ⇑f
def
ContinuousLinearMap.mkOfIsCompactOperator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[TopologicalAddGroup M₁]
[ContinuousConstSMul 𝕜₁ M₁]
[TopologicalAddGroup M₂]
[ContinuousSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
:
Upgrade a compact LinearMap to a ContinuousLinearMap.
Equations
- ContinuousLinearMap.mkOfIsCompactOperator hf = { toLinearMap := f, cont := ⋯ }
Instances For
@[simp]
theorem
ContinuousLinearMap.mkOfIsCompactOperator_to_linearMap
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[TopologicalAddGroup M₁]
[ContinuousConstSMul 𝕜₁ M₁]
[TopologicalAddGroup M₂]
[ContinuousSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
:
@[simp]
theorem
ContinuousLinearMap.coe_mkOfIsCompactOperator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[TopologicalAddGroup M₁]
[ContinuousConstSMul 𝕜₁ M₁]
[TopologicalAddGroup M₂]
[ContinuousSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
:
theorem
ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[NontriviallyNormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
[RingHomIsometric σ₁₂]
{M₁ : Type u_3}
{M₂ : Type u_4}
[TopologicalSpace M₁]
[AddCommGroup M₁]
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[TopologicalAddGroup M₁]
[ContinuousConstSMul 𝕜₁ M₁]
[TopologicalAddGroup M₂]
[ContinuousSMul 𝕜₂ M₂]
{f : M₁ →ₛₗ[σ₁₂] M₂}
(hf : IsCompactOperator ⇑f)
:
ContinuousLinearMap.mkOfIsCompactOperator hf ∈ compactOperator σ₁₂ M₁ M₂
theorem
isClosed_setOf_isCompactOperator
{𝕜₁ : Type u_1}
{𝕜₂ : Type u_2}
[NontriviallyNormedField 𝕜₁]
[NormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[AddCommGroup M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[UniformSpace M₂]
[UniformAddGroup M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
[CompleteSpace M₂]
:
IsClosed {f : M₁ →SL[σ₁₂] M₂ | IsCompactOperator ⇑f}
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}
[NontriviallyNormedField 𝕜₁]
[NormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3}
{M₂ : Type u_4}
[SeminormedAddCommGroup M₁]
[AddCommGroup M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[UniformSpace M₂]
[UniformAddGroup M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
[CompleteSpace M₂]
:
(compactOperator σ₁₂ M₁ M₂).topologicalClosure = compactOperator σ₁₂ M₁ M₂
theorem
isCompactOperator_of_tendsto
{ι : Type u_1}
{𝕜₁ : Type u_2}
{𝕜₂ : Type u_3}
[NontriviallyNormedField 𝕜₁]
[NormedField 𝕜₂]
{σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_4}
{M₂ : Type u_5}
[SeminormedAddCommGroup M₁]
[AddCommGroup M₂]
[NormedSpace 𝕜₁ M₁]
[Module 𝕜₂ M₂]
[UniformSpace M₂]
[UniformAddGroup M₂]
[ContinuousConstSMul 𝕜₂ M₂]
[T2Space M₂]
[CompleteSpace M₂]
{l : Filter ι}
[l.NeBot]
{F : ι → M₁ →SL[σ₁₂] M₂}
{f : M₁ →SL[σ₁₂] M₂}
(hf : Filter.Tendsto F l (nhds f))
(hF : ∀ᶠ (i : ι) in l, IsCompactOperator ⇑(F i))
: