Theorem 1.3

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.continuous_regular_spectral_correspondence

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

prove2quantum

Let $M$ be Hausdorff. Every continuous $f:M\to\mathbb R$ induces the regular spectral family

\sigma_f(\lambda)=\operatorname{int}\bigl(f^{-1}(({-\infty},\lambda])\bigr).

Its admissible domain is all of $M$ , and its induced function is $f$ . Conversely, for every regular spectral family $\sigma$ , the domain $D(\sigma)$ is open and dense, all pointwise cuts there are finite, and $f_\sigma:D(\sigma)\to\mathbb R$ is continuous. The family induced by this function in the subspace topology is $\sigma(\lambda)\cap D(\sigma)$ for every real $\lambda$ . This correspondence imposes neither compactness nor boundedness.

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

/-- Theorem 1.3; de Groote, Observables I, PDF p./pp. 14.
-/
theorem continuous_regular_spectral_correspondence {M : Type u} [TopologicalSpace M] [T2Space M] :
    (∀ f : M → ℝ, Continuous f → IsRegularSpectralFamily (openSublevels f) ∧
      admissibleDomain (openSublevels f) = Set.univ ∧
      spectralCutInfimum (fun t => (openSublevels f t : Set M)) = f) ∧
    (∀ E : ℝ → Opens M, IsRegularSpectralFamily E →
      IsOpen (admissibleDomain E) ∧ Dense (admissibleDomain E) ∧
      Continuous (fun x : admissibleDomain E => spectralCutInfimum (fun t => (E t : Set M)) x.val) ∧
      (∀ x ∈ admissibleDomain E, {t | x ∈ (E t : Set M)}.Nonempty ∧
        BddBelow {t | x ∈ (E t : Set M)}) ∧
      ∀ t : ℝ,
        (openSublevels (fun x : admissibleDomain E =>
          spectralCutInfimum (fun s => (E s : Set M)) x.val) t : Set (admissibleDomain E)) =
        {x | x.val ∈ (E t : Set M)}) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 14, Theorem 1.3

Read-back

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

For every Hausdorff topological space $M$ , define $O_f(t)=\operatorname{int}_M\{x:f(x)\le t\}$ for a function $f:M\to\mathbb R$ , and define $c_E(x)=\inf\{t:x\in E(t)\}$ for a family $E$ of open sets, using the total real infimum, which returns $0$ on an empty set or a set unbounded below. Here a regular spectral family $E:\mathbb R\to\operatorname{Opens}(M)$ means that $E$ is increasing, $E(t)=\operatorname{int}_M(\bigcap_{s>t}E(s))$ for every $t$ , $\operatorname{int}_M(\bigcap_t E(t))=\varnothing$ , $\bigcup_t E(t)=M$ , and $\overline{E(t)}\subseteq E(s)$ whenever $t<s$ ; set $D_E=\{x\in M:\exists t,\ x\notin E(t)\}$ . The theorem asserts both that every continuous $f:M\to\mathbb R$ has $O_f$ a regular spectral family, $D_{O_f}=M$ , and $c_{O_f}=f$ , and that every regular spectral family $E$ has $D_E$ open and dense in $M$ , has the function $g:D_E\to\mathbb R$ given by $g(x)=c_E(x)$ continuous in the subspace topology, has $\{t:x\in E(t)\}$ nonempty and bounded below for every $x\in D_E$ , and satisfies, for every $t\in\mathbb R$ ,

\operatorname{int}_{D_E}\{x\in D_E:g(x)\le t\}=\{x\in D_E:x\in E(t)\}.

The interior in this last equality is relative to $D_E$ ; the space $M$ is allowed to be empty, and no boundedness assumption on $f$ or $E$ is imposed.

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