What topological_space is used in B(ℝ)?

Stream: new members

[Lars Ericson]

The result of

#check @borel_space ℝ

is

borel_space ℝ : Π [_inst_1 : topological_space ℝ] [_inst_2 : measurable_space ℝ], Prop

If I do #print instances topological_space there is no instance of topological_space ℝ.

On the other hand #print instances measurable_space produces real.measurable_space.

The definition for real.borel_space doesn't say what instance of topological_space ℝ is chosen, it just says

instance real.borel_space : borel_space ℝ := ⟨rfl⟩

How do I tell whattopological_space ℝ instance was chosen or constructed for real.borel_space?

[Heather Macbeth]

I believe it's from docs#real.metric_space

[Heather Macbeth]

You can do

import analysis.normed_space.basic

noncomputable def foo : topological_space ℝ := by apply_instance

#print foo

and trace it backwards.

[Lars Ericson]

I am trying to figure out how to fill out the arguments to @borel_space, which says it wants an [_inst_1 : topological_space ℝ] . However the result of

noncomputable def foo : topological_space ℝ := by apply_instance
#print foo

is

@[instance]
protected def foo : borel_space ℝ :=
{measurable_eq := rfl real.measurable_space}

The sequence of definitions appears to be looping borel_space requires topological_space which reduces to borel_space. But neither is declared as an alias of the other in mathlib:

class borel_space (α : Type*) [topological_space α] [measurable_space α] : Prop :=
(measurable_eq : ‹measurable_space α› = borel α)

@[protect_proj] structure topological_space (α : Type u) :=
(is_open        : set α → Prop)
(is_open_univ   : is_open univ)
(is_open_inter  : ∀s t, is_open s → is_open t → is_open (s ∩ t))
(is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))

attribute [class] topological_space

[Adam Topaz]

The class borel_space requires topological_space as an input, and it does not extend topological_space. So whatever lean finds for the topological_space is the instance that is used. I assume the whole point of the borel_space class is so that you have have measurable spaces which also happen to be topological spaces without requiring the sigma algebra to be the Borel algebra.

[Lars Ericson]

@Heather Macbeth 's answer is perfect. I didn't see it to begin with because I ran it in a context where borel_space was imported.

However if you just do import analysis.normed_space.basic as she does then it works and gives

noncomputable def foo : topological_space ℝ :=
uniform_space.to_topological_space

So the answer is that ℝ can be seen as a uniform_space and then transformed into a topological_space. ℝ is not a uniform_space out of the box, so we can repeat the exercise:

noncomputable def foo1 : uniform_space ℝ := by apply_instance
#print foo1

This gives

noncomputable def foo1 : uniform_space ℝ :=
metric_space.to_uniform_space'

and real.metric_space is in mathlib.

So that's the chain: metric_space to uniform_space to topological_space to borel_space. Nice!

[Lars Ericson]

Thank you @Heather Macbeth !!

[Adam Topaz]

If I understand the comments above, the topology on R comes from the metric_space sructure, which induces a uniform_space structure which then induces a topological_space structure.

[Adam Topaz]

I think the borel_space is separate.

[Adam Topaz]

There is a borel_space instance declared explicitly in docs#real.borel_space

[Adam Topaz]

For example:

import measure_theory.borel_space

example {α : Type*} [topological_space α] : borel_space α := by apply_instance -- fails

[Lars Ericson]

Yes it only got in there because I was looking at @borel_space and what arguments it requires. You can just say borel_space ℝ and it works. But I wanted to know how to fill in all the slots without using _ in @borel_space. When you run Heather's technique in a context where borel_space is imported, it is not informative. When you run it where only import analysis.normed_space.basic is imported, it is informative.

[Adam Topaz]

import measure_theory.borel_space

variables {α : Type} [topological_space α]

example : borel_space α := by apply_instance -- fails

instance foo1 : measurable_space α := borel α

instance foo2 : borel_space α := ⟨rfl⟩

example : borel_space α := by apply_instance -- now it works.

[Adam Topaz]

Maybe that example is more helpful in understanding what's happening...

[Lars Ericson]

I am trying to figure out how to make borel_space of the real interval [0,1].

[Adam Topaz]

What's your definition of [0,1]?

[Lars Ericson]

The set {x : 0 \leq x \leq 1}.

[Adam Topaz]

import measure_theory.borel_space
import data.set.intervals.basic

noncomputable theory

def I : Type* := set.Icc (0 : ℝ) 1
instance foo0 : topological_space I := by {unfold I, apply_instance}
instance foo1 : measurable_space I := borel I
instance foo2 : borel_space I := ⟨rfl⟩

example : borel_space I := by apply_instance -- now it works.

[Adam Topaz]

I was asking how you defined [0,1] in lean :) I assume it's approximately the subtype I defined above.

[Lars Ericson]

So I have to make sure in the constructor

borel_space : Π (α : Type u_1) [_inst_1 : topological_space α] [_inst_2 : measurable_space α], Prop

that I have a type for [0,1] like set.Icc 0 1 and a topological_space instance of [0,1] and a measurable_space instance of [0,1].

[Adam Topaz]

Note that set.Icc is a set, not a type. But since I declared it to be a type using the type ascription for I, lean automatically made into a type with the subtype construction.

[Lars Ericson]

That's why I was trying to figure out where the topological_space ℝ was proven so that I could figure out how to prove topological_space (set.Icc 0 1).

[Adam Topaz]

I assume that the topological space instance on a subset of a topological space is the one given by the subspace topology (that's the sensible thing), but I didn't check explicitly.

[Lars Ericson]

I'm trying to learn all these pieces.

[Adam Topaz]

Are you using vscode?

[Lars Ericson]

Yes, I'm just trying your example. It works, thanks!

[Adam Topaz]

If so, paste the following code, and click the link that show_term gives.

import topology.constructions

def foo {α : Type*} [topological_space α] (S : set α) : topological_space S := by show_term {apply_instance}

[Adam Topaz]

That's another trick to get the definition of the instance.

[Lars Ericson]

That's great, thank you!

[Adam Topaz]

If you do that, you can see that the set is given the subspace topology from docs#subtype.topological_space

[Lars Ericson]

I am trying to make the structure ([0,1], B([0,1]), P) where P is the real volume restricted to [0,1]. So, a probability space.

[Lars Ericson]

So

import measure_theory.lebesgue_measure
#check measure_theory.real.measure_space.volume -- measure_theory.measure_space.volume : measure_theory.measure ℝ

[Adam Topaz]

I suspect something like this is somewhere in mathlib already. Hopefully someone with more familiarity of the measure_theory library would help...

[Lars Ericson]

Almost all there:

import measure_theory.lebesgue_measure
import measure_theory.borel_space
import data.set.intervals.basic
import measure_theory.measure_space

open measure_theory

noncomputable theory

def I : Type* := set.Icc (0 : ℝ) 1
instance foo0 : topological_space I := by {unfold I, apply_instance}
instance foo1 : measurable_space I := borel I
instance foo2 : borel_space I := ⟨rfl⟩
#check foo2

def B01 : borel_space I := by apply_instance -- now it works.
#check B01

def μ := measure_theory.real.measure_space.volume
#check μ -- μ : measure_theory.measure ℝ

#check probability_measure μ -- probability_measure μ : Prop

[Lars Ericson]

There is no official structure in mathlib for probability_space but there is probability_measure and measure_space so that's about it.

[Lars Ericson]

I have to subtype measure_theory.real to [0,1] and the act of subtype should bless the volume as being subtype.

[Mario Carneiro]

The easiest way to check all these things is like so:

import measure_theory.lebesgue_measure
import measure_theory.borel_space
import data.set.intervals.basic
import measure_theory.measure_space

open measure_theory

#check (by apply_instance : topological_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : measurable_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : borel_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : measure_space (set.Icc (0 : ℝ) 1)) -- not ok :(

So it appears that it has not yet been proven that subtypes induce a measure.

[Mario Carneiro]

However, I do see map and comap and restrict among the measure constructions in measure_theory.measure_space, so it should not be hard to build the instance

[Mario Carneiro]

import measure_theory.lebesgue_measure
import measure_theory.borel_space
import data.set.intervals.basic
import measure_theory.measure_space

open measure_theory

noncomputable instance {α} {p : α → Prop} [m : measure_space α] : measure_space (subtype p) :=
{ volume := measure.comap (coe : _ → α) volume }

#check (by apply_instance : topological_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : measurable_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : borel_space (set.Icc (0 : ℝ) 1)) -- ok
#check (by apply_instance : measure_space (set.Icc (0 : ℝ) 1)) -- ok :)

[Johan Commelin]

what's the diff between line -2 and -4?

[Johan Commelin]

are you just making lean recompute instances for the lulz?

[Mario Carneiro]

just making double sure

[Mario Carneiro]

and here's how we show it is a probability space:

theorem subtype.volume_apply {α} {p : α → Prop} [measure_space α]
  (hp : is_measurable {x | p x}) {s : set (subtype p)} (hs : is_measurable s) :
  volume s = volume ((coe : _ → α) '' s) :=
measure.comap_apply _ subtype.coe_injective (λ _, is_measurable.subtype_image hp) _ hs

instance : probability_measure (volume : measure (set.Icc (0 : ℝ) 1)) :=
{ measure_univ := begin
    refine (subtype.volume_apply is_measurable_Icc is_measurable.univ).trans _,
    suffices : volume (set.Icc (0:ℝ) 1) = 1, {simpa},
    rw [real.volume_Icc], simp
  end }

[Lars Ericson]

GIven that probability_space itself is not currently in mathlib, would this be a reasonable definition:

import measure_theory.measure_space
open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

[Mario Carneiro]

yes

[Lars Ericson]

Thank you very much @Mario Carneiro, the Steinhaus space is born:

import measure_theory.lebesgue_measure
open measure_theory
noncomputable theory

instance {α} {p : α → Prop} [m : measure_space α] : measure_space (subtype p) :=
{ volume := measure.comap (coe : _ → α) volume }

theorem subtype.volume_apply {α} {p : α → Prop} [measure_space α]
  (hp : is_measurable {x | p x}) {s : set (subtype p)} (hs : is_measurable s) :
  volume s = volume ((coe : _ → α) '' s) :=
measure.comap_apply _ subtype.coe_injective (λ _, is_measurable.subtype_image hp) _ hs

abbreviation I01 := (set.Icc (0 : ℝ) 1)

instance P_I01 : probability_measure (volume : measure I01) :=
{ measure_univ := begin
    refine (subtype.volume_apply is_measurable_Icc is_measurable.univ).trans _,
    suffices : volume I01 = 1, {simpa},
    rw [real.volume_Icc], simp
  end }

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

instance Steinhaus : probability_space I01 :=
{ is_probability_measure := P_I01 }

#check Steinhaus -- PS_I01 : probability_space ↥I01

[Lars Ericson]

@Mario Carneiro would it make sense to put the above definition of probability_space into mathlib, and if so, how?

import measure_theory.measure_space
open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

[Mario Carneiro]

Yes, but it should come with a bunch of basic theorems about probability spaces

[Johan Commelin]

@Lars Ericson there is a video on how to make a PR to mathlib in the tutorial playlist on youtube: https://www.youtube.com/watch?v=Bnc8w9lxe8A&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=6

[Johan Commelin]

But like Mario said, every definition should come with an API around it.

[Lars Ericson]

Do you have a style guide for what should come with the API? There are things you can do with probability spaces, like create one from a distribution, but for the idea itself, there is not much more that I know except what is in the definition, i.e. that it is a measure space whose volume is a probability measure.

So I would put it in the file with probability_measure as a start. I can do a PR for that.

[Kevin Buzzard]

Take a look at any structure at all, preferably one you understand, and then look at all the lemmas proved immediately after the definition. That's the style guide. A thorough treatment of basic lemmas, preferably with very short proofs, all building on each other.

[Johan Commelin]

@Lars Ericson the start should include all the lemmas that are never written down in any other resource. Stuff like: P(A) <= 1 for all A

[Johan Commelin]

All these stupid basic facts

[Johan Commelin]

probability of A-complement, is 1 - P(A)

[Johan Commelin]

(Note that I don't know anything about probability theory.)

[Riccardo Brasca]

As a new user that recently wrote his first definition, with relative API, what guided me is the principle that if the API is good nobody should ever have to look at the actual definition (unless for doing advanced things of course).

[Adam Topaz]

A couple more things that could be added to the API:

1. The existence of binary products / coproducts.
2. The obvious instance on pempty and punit.

[Adam Topaz]

Another suggestion might be to introduce some useful synonyms, similar to the following:

import data.set.intervals
import data.real.basic
import measure_theory.measure_space
open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure:  probability_measure volume)

def Bernoulli (p : set.Icc (0 : ℝ) 1) := bool

namespace probability_space

instance {p : set.Icc (0 : ℝ) 1} : probability_space (Bernoulli p) := sorry

end probability_space

[Lars Ericson]

P(A) <= 1 is the essence of the definition of probability_measure. So it doesn't go in probability_space, it comes as a consequence of the fact that probability_space calls for a measure_space with a measure which is a probability_measure. So that doesn't seem like a good example of something I would say in the API for probability_space.

My sense (expressed by somebody here) is that most proper mathematicians consider probability space to be a forgettable and somewhat trivial concept. You define it once, then never talk about it. So there wouldn't be a lot of theorems to go in the API.

One thing you could say is that if

• (Ω,𝔸,P) is a probability space, and
• (S,Σ) is a measurable space, and
• X: (Ω,𝔸)→(S,Σ) is a random variable, and

• μ(X) : Σ → [0,1] is the distribution of X,
  then

• (S,Σ,μ(X)) is a probability space which we can call the distribution_space of X. But I don't know if you'd call that a theorem about probability_space or another type class that you'd need to define.

[Lars Ericson]

Of course once you got that far you'd want to define distribution and random_variable, so yet more APIs which I don't see in mathlib at the moment.

[Johan Commelin]

Lars Ericson said:

P(A) <= 1 is the essence of the definition of probability_measure. So it doesn't go in probability_space, it comes as a consequence of the fact that probability_space calls for a measure_space with a measure which is a probability_measure. So that doesn't seem like a good example of something I would say in the API for probability_space.

It happens quite often that right after a definition, you state a couple of lemmas whose proof is rfl, just to make the definition easier to use.

The fact that something is "trivial" or "true by definition" doesn't mean it's not a good idea to include in the basic API.

[Mario Carneiro]

Adam Topaz said:

A couple more things that could be added to the API:

1. The existence of binary products / coproducts.
2. The obvious instance on pempty and punit.

I don't think pempty is a probability space

[Mario Carneiro]

The fact that something is "trivial" or "true by definition" doesn't mean it's not a good idea to include in the basic API.

In fact, this is exactly what should be in the first revision of the basic API. Make all the trivial observations

[Adam Topaz]

@Mario Carneiro of course, you're right.

[Adam Topaz]

It's the initial meeasure space.

[Adam Topaz]

(Unfortunately this means the category cannot have finite coproducts, unless you change the definition of a probability measure to assume that P(set.univ) = 1 with the additional assumption that the type is nonempty.)

[Kevin Buzzard]

Do analysts use this category theory language anyway?

[Adam Topaz]

Maybe not ;)

[Kevin Buzzard]

Disjoint Union of two measure 1 things has measure 2 I guess

[Adam Topaz]

You have to average them.

[Adam Topaz]

So for example the coproduct of punitwith itself is a coin flip

[Mario Carneiro]

I guess the general form of that is another giry monad

[Lars Ericson]

@Adam Topaz you don't have to change the definition of a probability measure to assume that P(set.univ)=1, because that is literally the exact definition of a probability measure in mathlib:

class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1)

[Adam Topaz]

Oh, we were talking about the empty set.

[Lars Ericson]

Well another axiom I would add to probability_space is that the sample space is inhabited, that's standard.

[Adam Topaz]

The axioms imply that the measure of the empty set is $0$, so as @Mario Carneiro mentioned the empty set cannot be a probability space with this definition.

[Adam Topaz]

Lars Ericson said:

Well another axiom I would add to probability_space is that the sample space is inhabited, that's standard.

This would be redundant (at least classically).

[Lars Ericson]

I'm looking for a reference but my understanding is that inhabited is a required property of the sample space. Wikipedia doesn't really come out and say it except to index the outcomes starting from 1.

[Adam Topaz]

If it's not inhabited, then the set is empty, and the measure of the whole space would be 0, but the axioms assume that it's 1. Since 0 is not 1 in the reals, it follows that the set must be inhabited. Of course, this is a classical argument.

[Lars Ericson]

There you go. In nlab they say "a probability space is a measure space (X,μ) whose measure μ is a probability distribution: its integral is ∫Xμ=1".

[Lars Ericson]

You could add as a theorem to mathlib that probability spaces are inhabited, by a proof about the integral.

[Lars Ericson]

That could go in the API.

[Eric Wieser]

If it's a classical argument, it should probably be a nonempty instance not an inhabited one

[Eric Wieser]

Since nonempty is proof of existence without claiming computability

[Lars Ericson]

Here is a short proof by Eric Wofsey. It doesn't involve reasoning about integrals. He reasons about sigma algebras and derives a contradiction:

"There exists no probability space for which Ω=∅ . A priori, given a set Ω and a 𝜎 -algebra Σ on Ω , there can be any number of different measures ℙ which make (Ω,Σ,ℙ) satisfy the axioms of a probability space--usually there are many different possible probability measures ℙ , but there might not be any at all! In the case that Ω=∅ , the only possible 𝜎 -algebra on Ω is Σ={∅} , and there is no function ℙ:Σ→[0,1] which satisfies the axioms of a probability measure (since the axioms force ℙ(∅) to be both 0 and 1 )".

[Mario Carneiro]

Here's a short proof: in pempty, univ = empty, so 1 = volume univ = volume empty = 0, contradiction

[Adam Topaz]

All our problems would be solved if we just defined probability spaces as measure spaces where the measure of univ is finite (but not necessarily one). (Just to be clear, I'm certainly not suggesting this is a good idea, rather that the category you would obtain in this way would be a bit nicer.)

[Lars Ericson]

Speaking of which, I found my nonempty set definition!

Screenshot-from-2020-12-14-17-49-42.png

She defines a couple of categories, and is happy that "at no point in this paper was the requirement that the sample space have measure 1 essential to a result"....except on line 1 where she says that the sample space is nonempty. But maybe one of her two categories gets you where you want to be.

There is more where that comes from. I'll put Terence Tao on top because he's a superstar:

• https://terrytao.wordpress.com/2014/06/28/algebraic-probability-spaces/
• https://golem.ph.utexas.edu/category/2018/09/a_categorical_look_at_random_v.html
• https://arxiv.org/pdf/1611.03630.pdf
• https://mathoverflow.net/questions/20740/is-there-an-introduction-to-probability-theory-from-a-structuralist-categorical
• https://www.jstor.org/stable/40587190?seq=1
• http://www.denotational.co.uk/drafts/heunen-kammar-staton-yang-staton-spaces.pdf

I've never ever understood category theory and how it makes life easier. I have seen category theoretic styling used in Scratchpad II/Axiom as a way of specifying what might otherwise be called interfaces or classes. Here are some notes:

• Aldor Design

Axiom was used by Wilfred Kendall at Warwick to implement stochastic differentials and Ito integrals. So this is also worth a look:

• Symbolic Itô calculus: An introduction