17
$\begingroup$

As the title said, I would like to know if constructive measure theory has been developed somewhere ?

I am more precisely interested in the (constructive) theory of completely continuous valuation on locale, or eventually in countably continuous valuation on locale.

I know how to do constructively the integration of positive lower semi-continuous function with respect to a positive valuation (with value in lower semi-continuous real number) and I want to know if this kind of things has already been written properly somewhere (in order to be quoted) ?

On a closely related subject, I also want to know if the fact that the set of projection of an abelian von-neuman algebra $A$ is a frame whose corresponding locale $NSp A$ is the classifying space of the theory of normal character of $A$ and that complex valued function on $NSp A$ can be identified with unbounded operator affiliated to $A$ has been already written properly somewhere ? (I often see these mentioned in article or on MO, but I have never see a 'quotable' proof published. )

PS : By 'constructively' I mean using intuitionist logic.

Thank you !

Improve this question
$\endgroup$

4 Answers 4

Reset to default
10
$\begingroup$

Steve Vickers’ A monad of valuation locales presents a strong monad on the category of locales, a localic analogue of the Giry monad. It is commutative, i.e. product valuations exist and a Fubini Theorem holds. Concrete representations are given for the tensor product of lattices and for the modular monoid. Vickers combines domain theoretic measure theory with insights from our paper above. His theory is geometric. One difference with our work is that we focus on valuations on compact regular locales which give integrals to the Dedekind reals, whereas in the general theory the integrals are only lower reals.

Improve this answer
$\endgroup$
11
$\begingroup$

Thierry Coquand and Bas Spitters have several papers on this topic, see Integrals and Valuations, and Metric Boolean Algebras and Constructive Measure Theory.

Improve this answer
$\endgroup$
0
6
$\begingroup$

You'll find some interesting work on this by Alex Simpson, as you can see by browsing around his web page. I also wrote a blog entry on Simpson's work on the space of random sequences.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Tom, thanks for the pointer to my work. Just to point out that, although I have given talks on this topic, the only thing I have published on the subject (my APAL 2012 paper "Measure, randomness and sublocales") used classical logic. $\endgroup$
    – Alex Simpson
    Commented Sep 10, 2013 at 15:02
1
$\begingroup$

An interesting recent possibility is in the work by Sam Sanders here in weak logical frameworks, inspired by the work of Simpson and Yokoyama.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .