PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SpectralPointMass

A `{0,1}`-valued, boundedly supported `WOTSpectralMeasure` is a point mass

Stage one of the missing piece flagged in `Irreducible.lean`'s `key` lemma: a boundedly σ-additive `{0,1}`-valued Borel measure on `ℝ` is a Dirac point mass. Built by bisecting the bounded support interval, always keeping the half with measure `1`, and taking the (real-number) limit of the resulting nested interval endpoints.

Main definitions

- `WOTSpectralMeasure.exists_forall_notMem_measure_eq_zero` : given a bounded support and a `{0,1}`-valued measure, there is a point `r` such that every measurable set avoiding `r` has measure `0`.

1 declaration

theorem

A $\{0, 1\}$ -valued Borel measure on $\mathbb{R}$ is a Dirac point mass

#exists_forall_notMem_measure_eq_zero

Let $\mu$ be a Borel measure on $\mathbb{R}$ that takes only the values $0$ and $1$ ; that is, for every measurable set $E \subseteq \mathbb{R}$ , $\mu(E) = 0$ or $\mu(E) = 1$ . Suppose that $\mu$ is boundedly supported, such that there exist real numbers $a, b$ with $a \le b$ for which $\mu([a, b]) = 1$ . Then there exists a point $r \in \mathbb{R}$ such that $\mu(\{r\}) = 1$ . Furthermore, for any measurable set $E$ , if $r \notin E$ , then $\mu(E) = 0$ .

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.SpectralPointMass

A `{0,1}`-valued, boundedly supported `WOTSpectralMeasure` is a point mass

Main definitions

A {0,1}\{0, 1\}{0,1}-valued Borel measure on R\mathbb{R}R is a Dirac point mass

A $\{0, 1\}$ -valued Borel measure on $\mathbb{R}$ is a Dirac point mass