Weak sequential compactness in a Hilbert space

A bounded sequence in a real Hilbert space has a subsequence along which every inner product converges, to the inner product against one fixed vector. This is the sequential form of Banach-Alaoglu on a reflexive space. The direct method of the calculus of variations runs on this compactness, with EllipticPdes.Embedding.rellichEmbL_isCompact_of_lt supplying the strong compactness at the lower exponent.

Mathlib has Banach-Alaoglu as WeakDual.isCompact_closedBall and the weak topology as WeakSpace, and stops short of the sequential statement, which needs the ball to be metrisable and so the space to be separable. The proof here avoids separability of the whole space by working inside the closed span of the sequence.

Three steps

• the diagonal: ⟪u n, u m⟫ lies in a fixed compact box for each m, so the sequence of functions m ↦ ⟪u n, u m⟫ lies in a compact subset of ℕ → ℝ, which is metrisable, and a subsequence converges pointwise;
• the extension: the vectors against which the inner products converge form a closed submodule, since the bound M makes the convergence uniform in the direction, and it contains the sequence, hence the closed span, hence everything by orthogonal decomposition;
• the limit: the resulting functional is linear and bounded by M, so Riesz representation names the weak limit.

Main declarations

• EllipticPdes.Analysis.exists_weakLimit: the weak sequential compactness statement.

References

James Guo, Partial Differential Equations, Theorem V.2.5.

theorem EllipticPdes.Analysis.exists_weakLimit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : ℕ → H} {M : ℝ} (hM : ∀ (n : ℕ), ‖u n‖ ≤ M) : ∃ (w : H) (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (v : H), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u (φ k)) v) Filter.atTop (nhds (inner ℝ w v))

Weak sequential compactness. A bounded sequence in a real Hilbert space has a subsequence whose inner products against every vector converge, to the inner products against one vector.

What a weak limit inherits

theorem EllipticPdes.Analysis.norm_weakLimit_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {u : ℕ → H} {w : H} {M : ℝ} (hM : ∀ (k : ℕ), ‖u k‖ ≤ M) (hw : ∀ (v : H), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ w v))) : ‖w‖ ≤ M

Weak lower semicontinuity of the norm. A bound along the sequence bounds the weak limit.

theorem EllipticPdes.Analysis.mem_of_weakLimit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {u : ℕ → H} {w : H} {K : Submodule ℝ H} (hK : IsClosed ↑K) (hu : ∀ (k : ℕ), u k ∈ K) (hw : ∀ (v : H), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ w v))) : w ∈ K

Stability of a closed subspace under weak limits.

theorem EllipticPdes.Analysis.norm_weakLimit_le_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {u : ℕ → H} {w : H} {m : ℝ} (hm : Filter.Tendsto (fun (k : ℕ) => ‖u k‖) Filter.atTop (nhds m)) (hw : ∀ (v : H), Filter.Tendsto (fun (k : ℕ) => inner ℝ (u k) v) Filter.atTop (nhds (inner ℝ w v))) : ‖w‖ ≤ m

The weak limit of a sequence whose norms converge is bounded by that limit.