\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{measurable locale}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{measure_and_probability_theory}{}\paragraph*{{Measure and probability theory}}\label{measure_and_probability_theory}

[[!include measure theory - contents]]

\hypertarget{measurable_locales}{}\section*{{Measurable locales}}\label{measurable_locales}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{in_classical_mathematics}{In classical mathematics}\dotfill \pageref*{in_classical_mathematics} \linebreak
\noindent\hyperlink{in_constructive_mathematics}{In constructive mathematics}\dotfill \pageref*{in_constructive_mathematics} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{borel_measurable_spaces}{Borel measurable spaces}\dotfill \pageref*{borel_measurable_spaces} \linebreak
\noindent\hyperlink{lebesgue_measurable_spaces}{Lebesgue measurable spaces}\dotfill \pageref*{lebesgue_measurable_spaces} \linebreak
\noindent\hyperlink{normalmeasures}{Measures}\dotfill \pageref*{normalmeasures} \linebreak
\noindent\hyperlink{related_work}{Related work}\dotfill \pageref*{related_work} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Measurable locales are certain [[locales]], which may serve as a basis for [[measure theory]] much as general locales serve as a basis for [[topology]] (especially in [[constructive mathematics]]). Specifically, a measurable locale is equivalent to a [[localisable measurable space]] (or [[dual equivalence|dual]] to a commutative [[von Neumann algebra]]).

Ironically, in [[constructive mathematics]], measurable locales are \emph{not} locales (except for the [[empty space]]), on pain of [[excluded middle]].

The concept appears to be due to [[Dmitri Pavlov]].

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

At present, there is no purely [[order theory|order-theoretic]] definition of measurable locales. However, there are a few other ways of defining them.

\hypertarget{in_classical_mathematics}{}\subsubsection*{{In classical mathematics}}\label{in_classical_mathematics}

First we give definitions appropriate for [[classical mathematics]].

As a preliminary step, consider the [[category]] $Comp Bool Alg_{sup}$ of [[complete boolean algebras]] and [[supremum]]-preserving [[homomorphisms]] of boolean algebras. This is a [[full subcategory]] of the category $Frm$ of [[frames]] and so its [[opposite category]] $Comp Bool Alg_{sup}^{op}$ is a full subcategory of the category [[Loc]] of locales. The category $Meas Loc$ of measurable locales is yet further a full subcategory of $Comp Bool Alg_{sup}^{op}$, so our job is simply to specify \emph{which} complete boolean algebras are the [[objects]] of this category. There are at least three equivalent ways of doing so.

\begin{enumerate}%
\item By one definition, a complete boolean algebra $L$ is a \textbf{measurable locale} if there is a [[complete measure space]] $X$ such that $L$ is [[isomorphic]] (as a boolean algebra) to the boolean algebra $\mathcal{M}/\mathcal{N}$ of [[measurable subsets]] of $X$ modulo [[null subsets]]. Note that the measure on $X$ is irrelevant except to specify the null subsets. In this way, $Meas Loc$ becomes [[equivalence of categories|equivalent]] to the category $Loc Meas$ of [[localisable measurable spaces]]. (Not every measure space has a \emph{complete} boolean algebra as $\mathcal{M}/\mathcal{N}$; those which do are called \emph{localisable}, and we interpret the term `localisable measurable space' to refer to a structure with both $\mathcal{M}$ and $\mathcal{N}$ specified.)


\item By another definition, a complete boolean algebra $L$ is a \textbf{measurable locale} if for every element $x \neq 0$ of $L$ there is a [[normal measure]] (see \hyperlink{normalmeasures}{below}) $\mu$ on $L$ valued in $[0,\infty]$ such that $\mu(x) = 1$. (It would be enough to demand that $0 \lt \mu(x) \lt \infty$, since we can rescale the measure.)


\item By yet another definition, a complete boolean algebra $L$ is a \textbf{measurable locale} if there is a commutative $W^*$-[[W-star-algebra|algebra]] $A$ such that $L$ is [[isomorphic]] (as a boolean algebra) to the boolean algebra $Proj(A)$ of [[projection operator]]s in $A$; (see [[idempotent operator]] for a construction of $Proj(A)$). In this way, $Meas Loc$ becomes [[dual equivalence|dual]] to the category $Comm W^* Alg$ of commutative $W^*$-algebras. For this definition, we need not require that $L \cong Proj(A)$ be complete (or even a boolean algebra); this can be proved.



\end{enumerate}
Whichever of these equivalent definitions is adopted, a \textbf{measurable function} between measurable locales is simply a [[continuous map]] between them as locales; these are the [[morphisms]] of $Meas Loc$. In more elementary terms, a measurable function from $L$ to $M$ (thought of as measurable locales) is a function from $M$ to $L$ (thought of as Boolean algebras) that preserves all [[joins]] (and then it also preserves finite [[meets]] and so is a [[frame]] [[homomorphism]]).

\hypertarget{in_constructive_mathematics}{}\subsubsection*{{In constructive mathematics}}\label{in_constructive_mathematics}

(This section is not due to Pavlov.)

For purposes of [[constructive mathematics]], [[Toby Bartels]] suspects that it is appropriate to use the definition from $W^\star$-algebras, so long as we allow norms to be [[lower real numbers]]. (If they are all [[located real number|located]], then $Proj(A)$ has [[decidable equality]], which we don't want to require.) The other definitions seem more difficult to work with (primarily because they require completeness explicitly).

For this definition (as was remarked above), we need not require that $L \cong Proj(A)$ be complete. Constructively, we \emph{cannot} require this; $Proj(A)$ need not be complete (although it is still a boolean algebra). Indeed, consider the point (see \hyperlink{examples}{the examples}), based on $A \coloneqq \mathbb{C}$, which is \emph{not} the complete [[Heyting algebra]] of \emph{all} [[truth values]] but only the (possibly incomplete) boolean algebra $\{\bot, \top\}$ of \emph{classical} truth values (corresponding to the self-adjoint idempotent complex numbers $0$ and $1$).

It seems that there is some notion of completeness that applies here; $L$ should in some sense be `measurably complete'. In the point, for example, the [[subsingleton]] $\{* \;|\; P\}$, where $P$ is a truth value, is measurable iff $P$ is true or false, so the supremum of $\{\top \;|\; P\}$ exists in $L$ under the same circumstances. Figuring this out could allow the definitions through measurable spaces or normal measures to work.

Simpson's theory of [[sigma-locale]]s, see below, is developed in classical framework, but could be a good starting point for a constructive theory, as it avoids the focus on complements.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

The [[empty space]], which is [[initial object|initial]] in $Meas Loc$, is the [[terminal object|terminal]] boolean algebra with one element.

The [[point]], which is [[terminal object|terminal]] in $Meas Loc$, is the [[initial object|initial]] boolean algebra $\{\bot, \top\}$ of (classical) [[truth values]].

The [[real line]] is the boolean algebra of Lebesgue-[[measurable sets]] of [[real numbers]] modulo the [[null sets]]. This is complete as a boolean algebra because \ldots{} [argument needed] (and even constructively, it is still a boolean algebra).

Applying the classification of $W^*$-algebras, we find that (up to [[isomorphism]]), every measurable locale is a [[disjoint union]] (dually a [[direct product]] of boolean algebras) of points or of points and infinitely many real lines; a single real line is already isomorphic to the union of countably infinitely many real lines. (Of course, we can't expect this [[classification theorem]] to hold constructively.)

\hypertarget{borel_measurable_spaces}{}\subsubsection*{{Borel measurable spaces}}\label{borel_measurable_spaces}

To do [[measure theory]], it's important to know how to interpret the [[real line]] with the [[Borel sets]] (rather than Lebesgue sets) as a measurable space. This is actually a little tricky, because [[Lebesgue measure]] is not complete on the Borel sets, and passing to the Lebesgue sets gives a different measurable space. We might simply take the Borel sets as they are (so that only the empty set is null), but then this is not complete as a boolean algebra.

One might suspect that there is no Borel real line in $Meas Loc$, which would cast serious doubts on that as a category for measure theory. But we can argue by [[abstract nonsense]] that it must exist, and more generally that any [[locale]] (including the [[locale of opens]] of any [[topological space]]) has a \textbf{Borel measurable locale}, as follows:

\ldots{} $<$http://mathoverflow.net/questions/31603/why-do-probabilists-take-random-variables-to-be-borel-and-not-lebesgue-measurab/31724\#31724{\tt \symbol{62}} \ldots{} [[representable functor theorem]] \ldots{}

In the case of the real line, the resulting measurable locale is actually rather complicated: something like an uncountable union of points and lines.

This process is a [[functor]] $B\colon Loc \to Meas Loc$, which we can also extend to $Top \to Loc \to Meas Loc$.

\hypertarget{lebesgue_measurable_spaces}{}\subsubsection*{{Lebesgue measurable spaces}}\label{lebesgue_measurable_spaces}

Similarly, [[smooth manifolds]] give rise to (much simpler!) measurable locales by taking the Lebesgue sets (possible since we know which sets are null sets on a smooth manifold). This process is a [[functor]] $L\colon SmoothMan_subm \to MeasLoc$, where the [[morphisms]] in $SmoothMan_subm$ are the [[smooth map|smooth]] [[submersions]].

In the case of the [[real line]], we get the usual line described under the basic examples above. In fact, \emph{any} [[second-countable space|second-countable]] smooth manifold with positive dimension gives rise to this measurable locale; the really interesting thing about $L$ is what it does to the morphisms.

\hypertarget{normalmeasures}{}\subsection*{{Measures}}\label{normalmeasures}

On \emph{any} complete boolean algebra $L$, given any [[abelian monoid]] $R$ equipped with a [[convergence space|convergence structure]] (such as $[0,\infty]$), a \textbf{[[normal measure]]} on $L$ valued in $R$ is a [[function]] $\mu\colon L \to R$ such that:

\begin{itemize}%
\item \emph{[[inclusion-exclusion|additivity]]}: $\mu(\bot) = 0$ and $\mu(x \wedge y) + \mu(x \vee y) = \mu(x) + \mu(y)$;


\item \emph{[[Scott continuity|continuity]]}: if $S$ is a downward-[[codirected set|directed]] [[subset]] of $L$ whose [[infimum]] is the [[bottom element]], then the [[net]] $(\mu(x))_{x\colon S}$ converges to $0$.



\end{itemize}
One could, of course, define a garden-variety [[measure]] by requiring continuity only when $S$ is the image of a decreasing [[sequence]], but apparently normal measures are what we want for measurable locales.

(Perhaps there is a theorem that absolutely continuous measures on, say, Lebesgue space correspond to normal measures on the real line as a measurable locale? Certainly [[Lebesgue measure]] is not normal on the $\sigma$-algebra of measurable sets, but presumably it is normal on the boolean algebra of measurable sets modulo null sets, which is what we want.)

I'm not entirely sure how this works in constructive mathematics, but $[0,\infty]$ (for a positive measure) would be the space of nonnegative [[lower reals]].

\hypertarget{related_work}{}\subsection*{{Related work}}\label{related_work}

This is related to [[sigma-locale]]s.

\begin{itemize}%
\item Alex Simpson, \emph{Measure, randomness and sublocales} \href{http://www.sciencedirect.com/science/article/pii/S0168007211001874}{link}

\end{itemize}
which is part of his work to develop [[synthetic probability theory]].

\hypertarget{references}{}\subsection*{{References}}\label{references}

The theory of measurable locales seems to be published entirely on MathOverflow, in various questions and answers by [[Dmitri Pavlov]]. Here is an index:

\begin{itemize}%
\item Dmitri Pavlov, \href{http://mathoverflow.net/questions/49426/is-there-a-category-structure-one-can-place-on-measure-spaces-so-that-category-th/49542#49542}{answer} to \emph{Is there a category structure one can place on measure spaces so that category-theoretic products exist?} (version: 2011-01-08)

\end{itemize}
Another post not in this index is:

\begin{itemize}%
\item Dmitri Pavlov, \emph{\href{http://mathoverflow.net/questions/71259/which-complete-boolean-algebras-arise-as-the-algebras-of-projections-of-commutati}{Which complete Boolean algebras arise as the algebras of projections of commutative von Neumann algebras?}} (version: 2011-07-25)

\end{itemize}
[[!redirects measurable locale]] [[!redirects measurable locales]]



\end{document}