theorem scaled_orthonormal_range_weaklySeqClosed_and_not_weaklyClosed {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] [CompleteSpace 𝓗] (e : ℕ → 𝓗) (he : Orthonormal ℝ e) (α : ℕ → ℝ) (hα_ge_one : ∀ (n : ℕ), 1 ≤ α n) (_hα_monotone : Monotone α) (hα_tendsto : Filter.Tendsto α Filter.atTop Filter.atTop) (hα_invSq_not_summable : ¬Summable fun (n : ℕ) => (α n)⁻¹ ^ 2) : IsClosed (Set.range fun (n : ℕ) => α n • e n) ∧ IsSeqClosed (⇑(toWeakSpace ℝ 𝓗) '' Set.range fun (n : ℕ) => α n • e n) ∧ ¬IsClosed (⇑(toWeakSpace ℝ 𝓗) '' Set.range fun (n : ℕ) => α n • e n) ∧ 0 ∈ closure (⇑(toWeakSpace ℝ 𝓗) '' Set.range fun (n : ℕ) => α n • e n) ∧ 0 ∉ Set.range fun (n : ℕ) => α n • e n

Example 3.33: for C = {α n • e n | n : ℕ} coming from an orthonormal sequence and a monotone weight sequence in [1, +∞) tending to +∞ with non-summable inverse squares, C is norm closed and weakly sequentially closed, is not weakly closed, and satisfies 0 ∈ closure ((toWeakSpace ℝ 𝓗) '' C) and 0 ∉ C.