Proposition 3.21

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.hilbert_stone_noncompact

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

If a complex Hilbert space $H$ has dimension greater than one, its closed-subspace Stone spectrum is not compact; in infinite dimension it is not locally compact:

\dim H>1\ \Longrightarrow\ Q(L(H))\text{ is noncompact},\qquad \dim H=\infty\ \Longrightarrow\ Q(L(H))\text{ is not locally compact}.

This does not claim that every point lacks a compact neighbourhood: atomic quasipoints remain isolated.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- Proposition 3.21; de Groote, Observables I, PDF p./pp. 65.
-/
theorem hilbert_stone_noncompact {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (hdim : 1 < Module.rank ℂ H) :
    ¬ CompactSpace (StoneSpectrum (ClosedSubmodule ℂ H)) ∧
      (¬ FiniteDimensional ℂ H → ¬ LocallyCompactSpace (StoneSpectrum (ClosedSubmodule ℂ H))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 65, Proposition 3.21

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $H$ be a complete complex inner product space whose complex module rank is strictly greater than $1$ . Consider the space of quasipoints of its closed complex-linear subspaces, where a quasipoint is a nonempty family excluding the zero subspace, every pair of its members contains a common member of the family, and the family is maximal under inclusion among families with these properties. Equip this space with the topology generated by the sets of quasipoints containing a specified closed subspace. Then this space is not compact. Furthermore, if $H$ is not finite-dimensional over $\mathbb C$ , this space is not locally compact. The noncompactness assertion also applies when $H$ is finite-dimensional of dimension at least $2$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph