Reason: First published proof of thm:l2-weak-compactness-2026a: nested selectors over a countable dense set (dependent choice), a diagonal subsequence, and Riesz-Frechet for the limit functional. Cauchy-Schwarz is referenced inline at the head of the proof as claims 4 and 5 of the inner-product lemma.
Step 2 (nested selectors). For every r and every n, Cauchy-Schwarz gives ∣⟨un,wr⟩L2∣≤C∥wr∥L2, so each real sequence (⟨un,wr⟩L2)n∈N is bounded.
We construct strictly increasing maps σr:N→N, each selecting a subsequence of the one selected by its predecessor. Since one selector is chosen at every stage, the construction is an application of Axiom of Dependent Choice: let P be the set of pairs (r,σ) with r∈N and σ:N→N strictly increasing such that (⟨uσ(n),ws⟩L2)n converges for every s≤r, and let a pair (r,σ) be related to (r+1,σ∘τ) whenever τ:N→N is strictly increasing and (⟨uσ(τ(n)),wr+1⟩L2)n converges. The paragraph that follows produces a starting element of P and shows that every element of P has a related successor in P, so that axiom yields a sequence of pairs whose second entries are the maps σr below. By Bolzano-Weierstrass Theorem for Real Sequences the bounded sequence (⟨un,w1⟩L2)n has a convergent subsequence; let σ1 be a strictly increasing map with (⟨uσ1(n),w1⟩L2)n convergent. If σr has been constructed, apply the same theorem to the bounded sequence (⟨uσr(n),wr+1⟩L2)n to obtain a strictly increasing τ with (⟨uσr(τ(n)),wr+1⟩L2)n convergent, and set σr+1=σr∘τ, again strictly increasing.
Step 3 (the diagonal subsequence). Put nj=σj(j). Writing σj+1=σj∘ρ with ρ strictly increasing, we have ρ(j+1)≥j+1 by the growth bound for strictly increasing sequences of natural numbers, so nj+1=σj(ρ(j+1))≥σj(j+1)>σj(j)=nj; thus n1<n2<… and (unj)j is a subsequence of (un)n.
Fix r. For j≥r we have nj=σr(θr,j(j)), and the index map j↦θr,j(j) is strictly increasing on {j∈N:j≥r}: if j′>j≥r then σr(θr,j′(j′))=nj′>nj=σr(θr,j(j)), and a strictly increasing map is order-reflecting: if θr,j′(j′)≤θr,j(j) then σr(θr,j′(j′))≤σr(θr,j(j)), contradicting the strict inequality just displayed. Writing j=r+i−1 with i∈N, the sequence (⟨unr+i−1,wr⟩L2)i∈N is obtained from (⟨uσr(n),wr⟩L2)n through the strictly increasing index map i↦θr,r+i−1(r+i−1), so it is a subsequence of a convergent sequence and converges, by A Subsequence of a Convergent Sequence Has the Same Limit. The sequence (⟨unj,wr⟩L2)j∈N agrees with it from index r onwards, and changing finitely many terms affects neither convergence nor the limit, since the condition of the definition of the limit concerns only sufficiently large indices. Hence (⟨unj,wr⟩L2)j∈N converges for every r∈N.
Step 4 (a bounded linear limit functional). Let v∈H. We claim that (⟨unj,v⟩L2)j is a Cauchy sequence. Let ε>0 be real and put δ=ε(3(C+1))−1, a positive real number. Since E is dense, Characterization of the Closure in a Metric Space by Open Balls provides r∈N with ∥v−wr∥L2<δ. For all i,j, linearity of the pairing, the triangle inequality for the absolute value and Cauchy-Schwarz give
and the first and third terms are at most Cδ<ε/3 each. The middle term is less than ε/3 for all large i,j: by step 3 the sequence (⟨unj,wr⟩L2)j converges, say to a, so there is J with ∣⟨unj,wr⟩L2−a∣<ε/6 for j≥J, and for i,j≥J the middle term is less than ε/3. Hence the sequence is Cauchy, and by Every Cauchy Sequence of Real Numbers Converges it converges. Define Λ(v) to be its limit; this defines a map Λ:H→R.
Λ is linear: for v,v′∈H and reals s,s′ one has ⟨unj,sv+s′v′⟩L2=s⟨unj,v⟩L2+s′⟨unj,v′⟩L2 by claim 4, and Arithmetic of Limits of Real Sequences gives Λ(sv+s′v′)=sΛ(v)+s′Λ(v′). Moreover −C∥v∥L2≤⟨unj,v⟩L2≤C∥v∥L2 for every j by Cauchy-Schwarz, so comparing with the two constant sequences and using claim 1 (comparison) of Order Properties of Limits of Real Sequences gives ∣Λ(v)∣≤C∥v∥L2.