Compactness in ℓ^p

19 fully proved

Restriction and zero extension

DefinitionRestriction of an \(\ell^p\) sequence to its first coordinates#✓fully proved

The restriction of an ℓ^p sequence to its first N coordinates.

def lpRestrict (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) : Fin N → 𝕜 :=
  fun i => x i

Used by 2

Used byPointwise action of the \(\ell^p\) restriction · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremPointwise action of the \(\ell^p\) restriction#✓fully proved

The restriction acts coordinatewise.

@[simp]
theorem lpRestrict_apply (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) (i : Fin N) :
    lpRestrict N x i = x i

Uses 1

Statement usesRestriction of an \(\ell^p\) sequence to its first coordinates

DefinitionZero extension of a finite coordinate vector#✓fully proved

The extension of a coordinate vector on Fin N by 0 to a total coordinate function on ℕ.

def lpExtend (N : ℕ) (z : Fin N → 𝕜) : ℕ → 𝕜 :=
  fun i => if h : i < N then z ⟨i, h⟩ else 0

Used by 2

Used byPointwise action of the zero extension · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremPointwise action of the zero extension#✓fully proved

The extension acts coordinatewise.

theorem lpExtend_apply (N : ℕ) (z : Fin N → 𝕜) (j : ℕ) :
    lpExtend N z j = if h : j < N then z ⟨j, h⟩ else 0

Uses 1 · Used by 1

Statement usesZero extension of a finite coordinate vector

Used byRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

Lifts and truncations

DefinitionLift of a coordinate function to a truncated \(\ell^p\) sequence#✓fully proved

The lift of a coordinate function on ℕ to an ℓ^p sequence, keeping only its first N coordinates.

noncomputable def lpLift (p : ℝ≥0∞) (N : ℕ) (y : ℕ → 𝕜) :
    lp (fun _ : ℕ => 𝕜) p :=
  ∑ i ∈ Finset.range N, lp.single (E := fun _ : ℕ => 𝕜) p i (y i)

Used by 4

Used byPointwise action of the finite \(\ell^p\) lift · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · Norm bound for the finite \(\ell^p\) lift · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

DefinitionTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates#✓fully proved

The all-p coordinate extension of finite truncation to the first N coordinates, also defined at p = ∞. For finite p ≥ 1, lpTrunc_eq_lpSchauderBasis_proj identifies it with the canonical continuous linear Schauder projection.

noncomputable def lpTrunc (p : ℝ≥0∞) (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    lp (fun _ : ℕ => 𝕜) p :=
  lpLift p N (fun i => x i)

Uses 1 · Used by 24

Statement usesLift of a coordinate function to a truncated \(\ell^p\) sequence

Used byTail of a single \(\ell^p\) vector can be made small · Pointwise action of \(\ell^p\) truncation · Truncation equals the Schauder basis projection · Truncation is a contraction on \(\ell^p\) · Tail of an \(\ell^p\) vector is no larger than the vector · Tails shrink as the truncation length grows · Truncations of an \(\ell^p\) vector converge to it · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\) · Uniform vanishing of tails · Truncations lie in the span of the first basis vectors · Tail norm identity for \(\ell^2\) truncation · Tail estimate for the Rellich ball · Rellich–Kondrachov, total boundedness form · Backward shift annihilates truncations after \(N\) steps · Dense periodic points of the Rolewicz operator for \(|\mu| > 1\) · Distance from the periodic approximant to the truncation · Norm of a term of the periodic approximant · Periodic approximant of a truncated sequence · Periodic approximant is a periodic point · Action of the scaled backward shift power on approximant terms · First term of the periodic approximant is the truncation · Summability of the geometric bound for periodic approximants · Summability of the shifted periodic approximant terms · Summability of the periodic approximant terms

TheoremPointwise action of the finite \(\ell^p\) lift#✓fully proved

The lift acts coordinatewise.

theorem lpLift_apply (N : ℕ) (y : ℕ → 𝕜) (j : ℕ) :
    lpLift p N y j = if j < N then y j else 0

Uses 1 · Used by 3

Statement usesLift of a coordinate function to a truncated \(\ell^p\) sequence

Used byPointwise action of \(\ell^p\) truncation · Norm bound for the finite \(\ell^p\) lift · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremPointwise action of \(\ell^p\) truncation#✓fully proved

Truncation acts coordinatewise.

theorem lpTrunc_apply (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) (j : ℕ) :
    lpTrunc p N x j = if j < N then x j else 0

Uses 2 · Used by 4

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPointwise action of the finite \(\ell^p\) lift

Used byTruncation is a contraction on \(\ell^p\) · Tail of an \(\ell^p\) vector is no larger than the vector · Tails shrink as the truncation length grows · Backward shift annihilates truncations after \(N\) steps

Norm

TheoremTruncation equals the Schauder basis projection#✓fully proved

For finite p ≥ 1, coordinate truncation is the canonical bundled Schauder-basis projection.

theorem lpTrunc_eq_lpSchauderBasis_proj (hp : p ≠ ⊤) (N : ℕ)
    (x : lp (fun _ : ℕ => 𝕜) p) :
    lpTrunc p N x = (lpSchauderBasis (𝕜 := 𝕜) hp).proj N x

Uses 3 · Used by 3

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · The unit vectors form a Schauder basis of ℓᵖ

Proof usesThe ℓᵖ partial-sum projections are truncations

Used byTruncation is a contraction on \(\ell^p\) · Truncations of an \(\ell^p\) vector converge to it · Truncations lie in the span of the first basis vectors

TheoremTruncation is a contraction on \(\ell^p\)#✓fully proved

Truncation is a contraction.

theorem norm_lpTrunc_le (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    ‖lpTrunc p N x‖ ≤ ‖x‖

Uses 5 · Used by 1

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPointwise action of \(\ell^p\) truncation · Truncation equals the Schauder basis projection · The unit vectors form a Schauder basis of ℓᵖ · The ℓᵖ partial-sum projections are contractions

Used byDistance from the periodic approximant to the truncation

TheoremTail of an \(\ell^p\) vector is no larger than the vector#✓fully proved

The tail of a vector is no larger than the vector itself.

theorem norm_sub_lpTrunc_le (N : ℕ) (x : lp (fun _ : ℕ => 𝕜) p) :
    ‖x - lpTrunc p N x‖ ≤ ‖x‖

Uses 2 · Used by 1

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPointwise action of \(\ell^p\) truncation

Used byRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremTails shrink as the truncation length grows#✓fully proved

Tails shrink as the truncation length grows.

theorem norm_sub_lpTrunc_mono {N M : ℕ} (h : N ≤ M) (x : lp (fun _ : ℕ => 𝕜) p) :
    ‖x - lpTrunc p M x‖ ≤ ‖x - lpTrunc p N x‖

Uses 2 · Used by 1

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesPointwise action of \(\ell^p\) truncation

Used byRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremNorm bound for the finite \(\ell^p\) lift#✓fully proved

The target ℓ^p norm of the finite lift is bounded by N ^ (1 / p) times the supremum norm of its first N coordinates. The norm on the source Pi type Fin N → 𝕜 is the supremum norm.

theorem norm_lpLift_le (hp : p ≠ ⊤) (N : ℕ) (y : ℕ → 𝕜) :
    ‖lpLift p N y‖ ≤ (N : ℝ) ^ (1 / p.toReal) * ‖fun i : Fin N => y i‖

Uses 2 · Used by 1

Statement usesLift of a coordinate function to a truncated \(\ell^p\) sequence

Proof usesPointwise action of the finite \(\ell^p\) lift

Used byRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremTruncations of an \(\ell^p\) vector converge to it#✓fully proved

The truncations of an ℓ^p vector converge to the vector.

theorem tendsto_lpTrunc (hp : p ≠ ⊤) (x : lp (fun _ : ℕ => 𝕜) p) :
    Tendsto (fun N => lpTrunc p N x) atTop (𝓝 x)

Uses 3 · Used by 2

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesTruncation equals the Schauder basis projection · The unit vectors form a Schauder basis of ℓᵖ

Used byTail of a single \(\ell^p\) vector can be made small · Dense periodic points of the Rolewicz operator for \(|\mu| > 1\)

TheoremTail of a single \(\ell^p\) vector can be made small#✓fully proved

The tail of a single vector can be made arbitrarily small.

theorem exists_norm_sub_lpTrunc_lt (hp : p ≠ ⊤) (x : lp (fun _ : ℕ => 𝕜) p)
    {ε : ℝ} (hε : 0 < ε) : ∃ N, ‖x - lpTrunc p N x‖ < ε

Uses 2 · Used by 1

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Proof usesTruncations of an \(\ell^p\) vector converge to it

Used byRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

DefinitionUniform vanishing of tails#✓fully proved

The tails of the elements of a set K vanish uniformly: for every ε > 0 there is N such that every x ∈ K is within ε of its truncation to the first N coordinates.

def UniformTailVanishing (p : ℝ≥0∞) (K : Set (lp (fun _ : ℕ => 𝕜) p)) : Prop :=
  ∀ ε > 0, ∃ N, ∀ x ∈ K, ‖x - lpTrunc p N x‖ < ε

Uses 1 · Used by 4

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates

Used byRiesz–Fréchet–Kolmogorov relative compactness criterion in \(\ell^p\) · Riesz–Fréchet–Kolmogorov criterion for compactness in \(\ell^p\) · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\) · Rellich–Kondrachov, total boundedness form

TheoremRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)#✓fully proved

The Riesz–Fréchet–Kolmogorov criterion for ℓ^p (ℕ, 𝕜), 1 ≤ p < ∞: a set is totally bounded if and only if it is bounded and its tails vanish uniformly.

theorem totallyBounded_iff_bounded_and_uniformTailVanishing (hp : p ≠ ⊤)
    {K : Set (lp (fun _ : ℕ => 𝕜) p)} :
    TotallyBounded K ↔ Bornology.IsBounded K ∧ UniformTailVanishing p K

Uses 11 · Used by 3

Statement usesUniform vanishing of tails

Proof usesTail of a single \(\ell^p\) vector can be made small · Zero extension of a finite coordinate vector · Pointwise action of the zero extension · Lift of a coordinate function to a truncated \(\ell^p\) sequence · Pointwise action of the finite \(\ell^p\) lift · Restriction of an \(\ell^p\) sequence to its first coordinates · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · Norm bound for the finite \(\ell^p\) lift · Tail of an \(\ell^p\) vector is no larger than the vector · Tails shrink as the truncation length grows

Used byRiesz–Fréchet–Kolmogorov relative compactness criterion in \(\ell^p\) · Riesz–Fréchet–Kolmogorov criterion for compactness in \(\ell^p\) · Rellich–Kondrachov, total boundedness form

TheoremRiesz–Fréchet–Kolmogorov criterion for compactness in \(\ell^p\)#✓fully proved

Compact form of the Riesz–Fréchet–Kolmogorov criterion.

theorem isCompact_iff_isComplete_and_bounded_and_uniformTailVanishing (hp : p ≠ ⊤)
    {K : Set (lp (fun _ : ℕ => 𝕜) p)} :
    IsCompact K ↔ IsComplete K ∧ Bornology.IsBounded K
      ∧ UniformTailVanishing p K

Uses 2

Statement usesUniform vanishing of tails

Proof usesRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

TheoremRiesz–Fréchet–Kolmogorov relative compactness criterion in \(\ell^p\)#✓fully proved

Relative-compact form of the Riesz–Fréchet–Kolmogorov criterion.

theorem isCompact_closure_iff_bounded_and_uniformTailVanishing (hp : p ≠ ⊤)
    {K : Set (lp (fun _ : ℕ => 𝕜) p)} :
    IsCompact (closure K) ↔ Bornology.IsBounded K ∧ UniformTailVanishing p K

Uses 2

Statement usesUniform vanishing of tails

Proof usesRiesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.