Compact operators and bounded sequences #
This file records sequential consequences of compactness for bounded sequences in normed spaces.
Main declarations #
IsCompactOperator.exists_subseq_tendsto: a compact operator sends a bounded sequence to a sequence with a convergent subsequence.IsCompactOperator.exists_dist_lt_of_norm_le: a compact operator cannot keep the images of a bounded sequence pairwise separated.
theorem
IsCompactOperator.exists_subseq_tendsto
{𝕜 : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
[NormedAddCommGroup Y]
[NormedSpace 𝕜 Y]
{K : X →L[𝕜] Y}
{R : ℝ}
{u : ℕ → X}
(hK : IsCompactOperator ⇑K)
(hu : ∀ (n : ℕ), ‖u n‖ ≤ R)
:
∃ (y : Y) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (fun (k : ℕ) => K (u (ψ k))) Filter.atTop (nhds y)
A compact operator sends a bounded sequence to a sequence with a convergent subsequence.
theorem
IsCompactOperator.exists_dist_lt_of_norm_le
{𝕜 : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
[NormedAddCommGroup Y]
[NormedSpace 𝕜 Y]
{K : X →L[𝕜] Y}
{R : ℝ}
{u : ℕ → X}
(hK : IsCompactOperator ⇑K)
(hu : ∀ (n : ℕ), ‖u n‖ ≤ R)
{ε : ℝ}
(hε : 0 < ε)
:
A compact operator cannot keep the images of a bounded sequence pairwise separated: two distinct indices always have images within any prescribed positive distance.