WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Compact operator

Revision #1097 → #2455 · back to history

modifiedCompact operator (normed spaces)3f1a4d04e425
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—`IsCompactOperator f := ∃ K, IsCompact K ∧ f ⁻¹' K ∈ 𝓝 0` is Mathlib's compact operator predicate, equivalent to the Wikipedia definition on normed spaces.
status—formalized
modifiedSequential characterization of compactnesse55acb3aeb1a
FieldFrom #1097To #2455
mathlib.decl—isCompactOperator_iff_isCompact_closure_image_closedBall
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—This iff characterization via the closed unit ball (and its `ball` sibling) is exactly the Wikipedia sequential characterization.
status—formalized
modifiedCompact implies bounded (normed)fd5db4553b4c
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.continuous
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—For a semilinear map, `IsCompactOperator ⇒ Continuous` (i.e. bounded) is proved directly.
status—formalized
modifiedTotally bounded characterization into Banach spacesabbf6846bb9a
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.isCompact_closure_image_of_bounded
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—The image of any bounded set has compact (hence totally bounded) closure; when the codomain is Banach this coincides with the Wikipedia total-boundedness statement.
status—formalized
modifiedCompact operator (TVS)8bb405dd62b1
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—`IsCompactOperator` is defined for arbitrary topological vector spaces via the neighborhood-of-zero characterization, with `isCompactOperator_iff_exists_mem_nhds_image_subset_compact` giving the image-of-neighborhood form.
status—formalized
modifiedFinite-rank operators are compacteda71a275183
FieldFrom #1097To #2455
mathlib.decl—isCompactOperator_of_locallyCompactSpace_rng
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—Mathlib has no `FiniteRank` predicate for operators, but any continuous linear map into a locally compact (e.g. finite-dimensional) space is compact, which subsumes the finite-rank case.
status—partial
modifiedIdentity compact iff finite-dimensionalb3fd3993b321
FieldFrom #1097To #2455
mathlib.decl—isCompactOperator_id_iff_finiteDimensional
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
note—Verbatim iff over a nontrivially normed field with `CompleteSpace 𝕜`.
status—formalized
modifiedInvertible compact operator forces finite-dimensionale2e2696f5e22
FieldFrom #1097To #2455
mathlib.decl—FiniteDimensional.of_isCompactOperator_id
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
note—Mathlib proves that if the identity is compact then the space is finite-dimensional, from which the invertible-compact-operator corollary is immediate, but the corollary itself is not stated as a lemma.
status—partial
modifiedCompact implies bounded and continuous8fa923b8a21e
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.continuous
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—Same lemma as (fd5db4553b4c): a compact linear map is automatically continuous.
status—formalized
modifiedCompact operators form a closed subspacee9e88cd67c76
FieldFrom #1097To #2455
mathlib.decl—isClosed_setOf_isCompactOperator
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—Together with the submodule `compactOperator` (add/smul/zero closure), this gives the closed-subspace structure of K(X,Y) in L(X,Y).
status—formalized
modifiedCompact operators are a two-sided idealc5aa0ec8d82a
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.clm_comp
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—Both `IsCompactOperator.comp_clm` (precompose) and `IsCompactOperator.clm_comp` (postcompose) with a CLM produce a compact operator — the two-sided-ideal property.
status—formalized
modifiedCalkin algebra and essential spectrum46a476fd9800
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Calkin algebra or essential-spectrum definition exists in Mathlib.
status—not_formalized
modifiedApproximation by finite-rank on Hilbert spacesfdfc09c32226
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no finite-rank operator concept and no approximation-by-finite-rank theorem for Hilbert-space compact operators.
status—not_formalized
modifiedEnflo counter-example to approximation property11379f224ca0
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The approximation property and Enflo's counter-example are not present in Mathlib.
status—not_formalized
modifiedSchauder's theorem83c7c3cffb44
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `IsCompactOperator.*adjoint` returns nothing; Schauder's theorem (T compact iff T* compact) is not in Mathlib.
status—not_formalized
modifiedRange of a compact operator is separable0671710af1cb
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `IsCompactOperator` lemma about separability of the range closure exists in Mathlib.
status—not_formalized
modifiedCompact implies strictly singularfff1e361bf29
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Strictly singular operators are not defined in Mathlib.
status—not_formalized
modifiedI − T is Fredholm of index zeroa19a47d60f63
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no Fredholm-operator definition or index; a TODO in `Banach.lean` explicitly notes this gap.
status—not_formalized
modifiedFredholm alternativefd579400b177
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.hasEigenvalue_or_mem_resolventSet
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
note—The Fredholm alternative is stated exactly: for a compact operator T and μ ≠ 0, either μ is an eigenvalue of T or μ lies in the resolvent set.
status—formalized
modifiedParameter-dependent Fredholm alternativec04997020a36
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.hasEigenvalue_iff_mem_spectrum
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
note—`hasEigenvalue_iff_mem_spectrum` says that for μ ≠ 0, μ is in the spectrum of a compact operator iff it is an eigenvalue — the parameter-dependent alternative.
status—formalized
added0 belongs to the spectrum of a compact operatora480519fa280
modifiedSpectrum of a compact operatorbdc1233608fb
FieldFrom #1097To #2455
mathlib.decl—IsCompactOperator.hasEigenvalue_iff_mem_spectrum
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
note—This lemma states exactly that the nonzero spectrum of a compact operator consists of its (nonzero) eigenvalues.
status—formalized
modifiedNonzero spectrum is finite or countable with 0 as only accumulationb4fcf4c18bc4
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib lemma states the finite-or-countable spectrum with 0-accumulation property for compact operators.
status—not_formalized
modifiedEqual kernel and cokernel dimensions613b444891a1
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Depends on Fredholm-index theory, which is not in Mathlib.
status—not_formalized
modifiedAdjoint shares nonzero spectrum6acd0694f6b3
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `IsCompactOperator` lemma relating the spectra of T and its adjoint exists in Mathlib.
status—not_formalized
modifiedOperator with compact resolventd99549cad0bf
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The notion of an unbounded operator with compact resolvent is not defined in Mathlib.
status—not_formalized
modifiedSpectral theorem for compact self-adjoint operatorsed0f855a114f
FieldFrom #1097To #2455
mathlib.decl—ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.InnerProductSpace.Spectrum
note—The eigenspaces of a compact self-adjoint operator span the ambient Hilbert space; combined with `finite_dimensional_eigenspace` and `hasEigenvalue_iff_mem_spectrum`, this is the compact-self-adjoint spectral theorem.
status—formalized
modifiedDiagonal representation of compact self-adjoint operatorb05f226827f9
FieldFrom #1097To #2455
mathlib.decl—ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.InnerProductSpace.Spectrum
note—The proof that eigenspaces span the whole Hilbert space is present, but the explicit orthogonal-direct-sum decomposition (an `IsHilbertSum` statement) for a compact self-adjoint operator is not.
status—partial
modifiedExtension to compact normal operatorsc58c8115a0f9
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No analogous spectral decomposition for compact normal (non-self-adjoint) operators is in Mathlib.
status—not_formalized
modifiedSingular-value decomposition of compact operators9bb34a69e785
FieldFrom #1097To #2455
mathlib.decl—LinearMap.singularValues
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.InnerProductSpace.SingularValues
note—Mathlib defines singular values only for maps between finite-dimensional inner-product spaces; SVD for general compact operators (the infinite-dimensional expansion) is not formalized.
status—partial
modifiedHilbert–Schmidt and trace-class operatorsa4526e07f6a4
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Hilbert–Schmidt and trace-class operators are not defined in Mathlib.
status—not_formalized
modifiedTrace-class ⊂ Hilbert–Schmidt ⊂ compact256b823f342e
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the trace-class nor the Hilbert–Schmidt operator ideal is present, so this inclusion chain is not formalized.
status—not_formalized
modifiedCompletely continuous operatorf5f77eda12c2
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The completely-continuous-operator predicate (weak→norm sequential continuity) is not defined.
status—not_formalized
modifiedCompact ⇒ completely continuous; converse on reflexive spacesc95a8901417b
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No comparison between compact and completely continuous operators is stated in Mathlib.
status—not_formalized
modifiedFinite-rank operators48ae110e472c
FieldFrom #1097To #2455
mathlib.decl—isCompactOperator_of_locallyCompactSpace_rng
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.Basic
note—No `FiniteRank` predicate exists, but any CLM into a locally compact (finite-dim) space is compact, which captures the finite-rank example.
status—partial
modifiedDiagonal/multiplication operators on sequence spaces5816f8522944
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Multiplication/diagonal operators on ℓᵖ with compactness characterization are not formalized.
status—not_formalized
modifiedIntegral operators with regular kernel8a42c62003c8
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No general integral-kernel operator with a compactness theorem is present in Mathlib.
status—not_formalized
addedHilbert–Schmidt integral operator on L²37d47ee97b3f
modifiedIdentity on infinite-dimensional Banach space is not compactc74f080b7a00
FieldFrom #1097To #2455
mathlib.decl—isCompactOperator_id_iff_finiteDimensional
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
note—The identity of an infinite-dimensional Banach space fails to be compact by the contrapositive of `isCompactOperator_id_iff_finiteDimensional`.
status—formalized
modifiedShift operators are not compact55a966a1dfcd
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Unilateral shift operators on ℓᵖ are not treated as a named example in Mathlib.
status—not_formalized
modifiedBounded operators into nuclear spaces are compact2b516adcadb6
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Nuclear spaces are not defined in Mathlib.
status—not_formalized
modifiedCauchy integral operatordb42cc1f36c4
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Cauchy integral operator as a specific compact-operator example is not present in Mathlib.
status—not_formalized
modifiedCompact embeddingb6fc930b8e46
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `CompactEmbedding` concept exists; one would have to state `IsCompactOperator (inclusion : X → Y)` by hand.
status—not_formalized
modifiedRellich–Kondrachov theorem63b40a858723
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Rellich–Kondrachov theorem is present in Mathlib.
status—not_formalized
modifiedLebesgue space inclusion is not compact400840cbec98
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The failure of compactness for Lᵖ ↪ Lq inclusions is not stated in Mathlib.
status—not_formalized
modifiedHardy space embeds compactly into holomorphic functions3e23709f5230
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Hardy spaces are not defined in Mathlib, so this compact-embedding example cannot be stated.
status—not_formalized
modifiedBergman space compact embedding134a8657c064
FieldFrom #1097To #2455
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Bergman spaces are not defined in Mathlib.
status—not_formalized