Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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 !

share|improve this question
add comment

3 Answers

up vote 3 down vote accepted

Vickers 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.

share|improve this answer
add comment

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

share|improve this answer
add comment

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.

share|improve this answer
    
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. –  Alex Simpson Sep 10 '13 at 15:02
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.