Rellich–Kondrachov theorem

DefinitionRellich weight#✓fully proved

The Rellich weight 1 + n ^ 2.

def rellichWeight (n : ℕ) : ℝ := 1 + (n : ℝ) ^ 2

Used by 6

Used byRellich–Kondrachov, closedness form · Membership in the Rellich ball via partial sums · Finitely supported sequences in the Rellich ball · Tail estimate for the Rellich ball · Rellich ball depends only on the absolute radius · Rellich–Kondrachov, total boundedness form

DefinitionMembership in the Rellich ball via partial sums#✓fully proved

Membership in the Rellich ball: every finite weighted partial sum is bounded by M ^ 2.

def memRellichBall (x : ℓ²(ℕ, 𝕜)) (M : ℝ) : Prop :=
  ∀ F : Finset ℕ, ∑ n ∈ F, rellichWeight n * ‖(x : ℕ → 𝕜) n‖ ^ 2 ≤ M ^ 2

Uses 1 · Used by 5

Statement usesRellich weight

Used byFinitely supported sequences in the Rellich ball · Tail estimate for the Rellich ball · Rellich ball of weighted square-summable sequences · Rellich ball depends only on the absolute radius · Rellich–Kondrachov, total boundedness form

DefinitionRellich ball of weighted square-summable sequences#✓fully proved

The Rellich ball of radius M: sequences in ℓ²(ℕ, 𝕜) whose weighted ℓ² energy is at most M ^ 2.

def rellichBall (M : ℝ) : Set (ℓ²(ℕ, 𝕜)) := {x | memRellichBall x M}

Uses 1 · Used by 5

Statement usesMembership in the Rellich ball via partial sums

Used byRellich–Kondrachov, sequential form · Rellich–Kondrachov, closedness form · Rellich–Kondrachov, compactness form · Rellich ball depends only on the absolute radius · Rellich–Kondrachov, total boundedness form

TheoremSquared \(\ell^2\) norm as a sum of squared coordinates#✓fully proved

The ℓ² norm squared is the sum of the squared coordinate norms.

theorem norm_sq_eq_tsum (x : ℓ²(ℕ, 𝕜)) :
    ‖x‖ ^ 2 = ∑' n, ‖(x : ℕ → 𝕜) n‖ ^ 2

Used by 2

Used byTail norm identity for \(\ell^2\) truncation · Rellich–Kondrachov, total boundedness form

TheoremFinitely supported sequences in the Rellich ball#✓fully proved

If x is supported in a finite set S and its weighted sum over S is at most M ^ 2, then x lies in the Rellich ball.

theorem memRellichBall_of_support {x : ℓ²(ℕ, 𝕜)} {S : Finset ℕ} {M : ℝ}
    (hS : ∀ n, (x : ℕ → 𝕜) n ≠ 0 → n ∈ S)
    (h : ∑ n ∈ S, rellichWeight n * ‖(x : ℕ → 𝕜) n‖ ^ 2 ≤ M ^ 2) :
    memRellichBall x M

Uses 2

Statement usesMembership in the Rellich ball via partial sums · Rellich weight

TheoremTail norm identity for \(\ell^2\) truncation#✓fully proved

The tail norm identity: the distance from x to its truncation is the ℓ² norm of the tail.

theorem norm_sub_lpTrunc_sq_eq {x : ℓ²(ℕ, 𝕜)} (N : ℕ) :
    ‖x - lpTrunc 2 N x‖ ^ 2 = ∑' n, ‖(x : ℕ → 𝕜) (n + N)‖ ^ 2

Uses 2 · Used by 1

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

Proof usesSquared \(\ell^2\) norm as a sum of squared coordinates

Used byTail estimate for the Rellich ball

TheoremTail estimate for the Rellich ball#✓fully proved

The tail estimate: the squared distance from x to its truncation is at most M ^ 2 / (1 + N ^ 2).

theorem norm_sub_lpTrunc_sq_le {x : ℓ²(ℕ, 𝕜)} {M : ℝ} (hx : memRellichBall x M)
    (N : ℕ) : ‖x - lpTrunc 2 N x‖ ^ 2 ≤ M ^ 2 / rellichWeight N

Uses 4 · Used by 1

Statement usesTruncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · Membership in the Rellich ball via partial sums · Rellich weight

Proof usesTail norm identity for \(\ell^2\) truncation

Used byRellich–Kondrachov, total boundedness form

TheoremTruncations lie in the span of the first basis vectors#✓fully proved

Canonical truncations land in the span of the first N basis vectors.

theorem lpTrunc_mem_span (N : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    lpTrunc 2 N x ∈ Submodule.span 𝕜
      ((fun i : ℕ => lp.single (E := fun _ : ℕ => 𝕜) 2 i (1 : 𝕜)) ''
        (Finset.range N : Set ℕ))

Uses 3

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 ℓᵖ

TheoremRellich ball depends only on the absolute radius#✓fully proved

The Rellich ball only depends on |M|, since the bound is on M ^ 2.

theorem rellichBall_abs (M : ℝ) :
    rellichBall (𝕜 := 𝕜) M = rellichBall (𝕜 := 𝕜) |M|

Uses 3 · Used by 1

Statement usesRellich ball of weighted square-summable sequences

Proof usesMembership in the Rellich ball via partial sums · Rellich weight

Used byRellich–Kondrachov, total boundedness form

TheoremRellich–Kondrachov, total boundedness form#✓fully proved

The Rellich ball is totally bounded in ℓ²(ℕ, 𝕜).

theorem totallyBounded_rellichBall (M : ℝ) :
    TotallyBounded (rellichBall (𝕜 := 𝕜) M)

Uses 9 · Used by 1

Statement usesRellich ball of weighted square-summable sequences

Proof usesUniform vanishing of tails · Truncation of an \(\ell^p\) sequence, zeroing all but its first coordinates · Riesz–Fréchet–Kolmogorov criterion for total boundedness in \(\ell^p\) · Membership in the Rellich ball via partial sums · Squared \(\ell^2\) norm as a sum of squared coordinates · Tail estimate for the Rellich ball · Rellich ball depends only on the absolute radius · Rellich weight

Used byRellich–Kondrachov, compactness form

TheoremRellich–Kondrachov, closedness form#✓fully proved

The Rellich ball is closed.

theorem isClosed_rellichBall (M : ℝ) : IsClosed (rellichBall (𝕜 := 𝕜) M)

Uses 2 · Used by 1

Statement usesRellich ball of weighted square-summable sequences

Proof usesRellich weight

Used byRellich–Kondrachov, compactness form

TheoremRellich–Kondrachov, compactness form#✓fully proved

The Rellich ball is compact in ℓ²(ℕ, 𝕜).

theorem isCompact_rellichBall (M : ℝ) : IsCompact (rellichBall (𝕜 := 𝕜) M)

Uses 3 · Used by 1

Statement usesRellich ball of weighted square-summable sequences

Proof usesRellich–Kondrachov, closedness form · Rellich–Kondrachov, total boundedness form

Used byRellich–Kondrachov, sequential form

TheoremRellich–Kondrachov, sequential form#✓fully proved

Every sequence in the Rellich ball has a subsequence converging in ℓ²(ℕ, 𝕜) to a point of the ball.

theorem exists_subseq_tendsto_of_memRellichBall (M : ℝ) {u : ℕ → ℓ²(ℕ, 𝕜)}
    (hu : ∀ n, u n ∈ rellichBall (𝕜 := 𝕜) M) :
    ∃ y ∈ rellichBall (𝕜 := 𝕜) M, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      Filter.Tendsto (u ∘ φ) Filter.atTop (𝓝 y)

Uses 2

Statement usesRellich ball of weighted square-summable sequences

Proof usesRellich–Kondrachov, compactness form

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.