IsCompactOperator.restrict
theorem IsCompactOperator.restrict :
∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
[inst_3 : Module R₁ M₁] {f : M₁ →ₗ[R₁] M₁},
IsCompactOperator ⇑f →
∀ {V : Submodule R₁ M₁} (hV : ∀ v ∈ V, f v ∈ V), IsClosed ↑V → IsCompactOperator ⇑(f.restrict hV)
This theorem states that in a semiring, if a compact operator (an endomorphism) preserves a closed submodule (it sends any vector in the submodule back into the submodule), then the restriction of this operator to that submodule is also a compact operator. This restriction is itself an endomorphism on the closed submodule. In simpler terms, if you have a compact transformation that keeps a certain closed subset stable, then when you apply the transformation only to elements of this subset, the resulting transformation is still compact.
More concisely: If a compact endomorphism of a module preserves a closed submodule, then its restriction to the submodule is also a compact endomorphism.
|
IsCompactOperator.isCompact_closure_image_of_isVonNBounded
theorem IsCompactOperator.isCompact_closure_image_of_isVonNBounded :
∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁]
[inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module 𝕜₁ M₁] [inst_7 : Module 𝕜₂ M₂]
[inst_8 : ContinuousConstSMul 𝕜₂ M₂] [inst_9 : T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsVonNBounded 𝕜₁ S → IsCompact (closure (⇑f '' S))
This theorem states that for any nontrivially normed field `𝕜₁`, seminormed ring `𝕜₂`, and a ring homomorphism `σ₁₂` from `𝕜₁` to `𝕜₂`, along with topological spaces `M₁` and `M₂` and modules over `𝕜₁` and `𝕜₂` respectively. Also, assuming that the scalar multiplication is continuous in `M₂` and that `M₂` is a Hausdorff space. Given a linear map `f` from `M₁` to `M₂`, if `f` is a compact operator, then for any set `S` in `M₁` that is Von Neumann bounded, the closure of the image of `S` under `f` is compact.
This theorem essentially connects several concepts from functional analysis, including compact operators, Von Neumann boundedness, and compactness of the closure of a set, establishing a relationship between them under these specific conditions.
More concisely: Given a compact operator `f` between normed spaces, the closure of the image of any Von Neumann bounded set under `f` is compact.
|
IsCompactOperator.restrict'
theorem IsCompactOperator.restrict' :
∀ {R₂ : Type u_2} [inst : Semiring R₂] {M₂ : Type u_5} [inst_1 : UniformSpace M₂] [inst_2 : AddCommMonoid M₂]
[inst_3 : Module R₂ M₂] [inst_4 : T0Space M₂] {f : M₂ →ₗ[R₂] M₂},
IsCompactOperator ⇑f →
∀ {V : Submodule R₂ M₂} (hV : ∀ v ∈ V, f v ∈ V) [hcomplete : CompleteSpace ↥V],
IsCompactOperator ⇑(f.restrict hV)
This theorem states that if a compact operator is such that it preserves a complete submodule, then its restriction to that submodule also maintains the property of being a compact operator. In the context of linear algebra in Lean 4, `restrict` is used to indicate the restriction of an endomorphism from a larger vector space to a smaller one. To prove that the restriction of a compact operator is also compact, you would apply the `IsCompactOperator.codRestrict` to the composite of your operator and the submodule's type inclusion, which is guaranteed to be compact by `IsCompactOperator.comp_clm`.
More concisely: If a compact linear operator preserves a complete submodule, then its restriction to that submodule is also a compact operator.
|
IsCompactOperator.image_subset_compact_of_isVonNBounded
theorem IsCompactOperator.image_subset_compact_of_isVonNBounded :
∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁]
[inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module 𝕜₁ M₁] [inst_7 : Module 𝕜₂ M₂]
[inst_8 : ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsVonNBounded 𝕜₁ S → ∃ K, IsCompact K ∧ ⇑f '' S ⊆ K
This theorem states that for a compact operator `f` from one topological vector space `M₁` over a normed field `𝕜₁` to another vector space `M₂` over a seminormed ring `𝕜₂`, if a set `S` in `M₁` is von Neumann bounded (meaning it is absorbed by every neighborhood of the zero vector in `M₁`), then there exists a compact set `K` in `M₂` such that the image of `S` under the operator `f` is contained within `K`. This essentially asserts that compact operators map von Neumann bounded sets to compact sets.
More concisely: For a compact operator between topological vector spaces over normed fields, the image of any von Neumann bounded set is contained in a compact set.
|
isClosed_setOf_isCompactOperator
theorem isClosed_setOf_isCompactOperator :
∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
{M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
[inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : UniformAddGroup M₂]
[inst_8 : ContinuousConstSMul 𝕜₂ M₂] [inst_9 : T2Space M₂] [inst_10 : CompleteSpace M₂],
IsClosed {f | IsCompactOperator ⇑f}
The theorem `isClosed_setOf_isCompactOperator` states that for any nontrivially normed field `𝕜₁`, normed field `𝕜₂`, seminormed add commutative group `M₁`, add commutative group `M₂`, assuming that `M₁` is a normed space over `𝕜₁`, `M₂` is a module over `𝕜₂`, `M₂` is a uniform space, a uniform add group, has continuous constant scalar multiplication with `𝕜₂`, is a Hausdorff space (T2 space), and is a complete space, then the set of all linear maps from `M₁` to `M₂` that are compact operators is a closed set. A compact operator here refers to a linear operator that maps bounded sets to relatively compact sets.
More concisely: The set of compact linear operators from a normed space over field `𝕜₁` to a complete, Hausdorff, uniformly convex Banach module `M₂` over field `𝕜₂` is a closed set.
|