Probability measure of B(R) and B([0,1])

Stream: Is there code for X?

[Lars Ericson]

mathlib has B(ℝ) and it has probability_measure:

import measure_theory.measure_space
import measure_theory.borel_space
open measure_theory

#check real.borel_space -- real.borel_space : borel_space ℝ
#check measure_theory.probability_measure -- probability_measure : measure ?M_1 → Prop

With these tools, how do we construct a probability measure P of B(ℝ)?

Suppose we have a closed unit interval Icc01 = [0,1]:

def Icc01 : set ℝ := set.Icc 0 1 -- [0,1]

In mathlib, how do we construct the Borel space B([0,1])?

Given that we have constructed B([0,1]), how do we construct a probability measure P of B([0,1]) such that for any subinterval [a,b] of [0,1], 0 ≤ a ≤ b ≤ 1, we have that P([a,b]) = b-a?

[Yury G. Kudryashov]

We already have the Lebesgue measure (available as the volume on \R).

[Yury G. Kudryashov]

If you restrict this measure to Icc 0 1, then you will have the desired measure. You'll have to prove a probability_measure instance.

[Lars Ericson]

mathlib doesn't have real.volume. It does have real.volume_Icc. I don't know how to apply it to [0,1]. This doesn't work:

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

#check real.volume_Icc -- real.volume_Icc : ⇑measure_theory.measure_space.volume (set.Icc ?M_1 ?M_2) = ennreal.of_real (?M_2 - ?M_1)
#check real.volume_Icc (set.Icc 0 1)

[Yury G. Kudryashov]

We have docs#measure_theory.measure_space.volume

[Yury G. Kudryashov]

And docs#measure_theory.real.measure_space

[Yury G. Kudryashov]

So, if you write (volume : measure \R), then you get the Lebesgue meaure on \R.

[Yury G. Kudryashov]

It seems that we don't have an instance subtype.measure_space yet. Adding this instance is a good exercise on understanding the definitions.

[Yury G. Kudryashov]

You should define it using docs#measure_theory.measure.comap and coercion.

[Lars Ericson]

With much help from you all I have constructed an instance of a measure_space:

import measure_theory.measure_space
open measure_theory

def X : Type := fin 3

instance : fintype X := fin.fintype _

def A1 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))

def M1 : measurable_space X :=
{ is_measurable' := A1.algebra,
  is_measurable_empty := by {rw A1, finish},
  is_measurable_compl := assume a h, by {rw A1 at *, finish},
  is_measurable_Union := assume f hf, by {rw A1 at *, simp },
}

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
  (λ s _, finset.card s.to_finset)
  (by simp)
  (λ x h a, begin
    simp,
    sorry
  end)

noncomputable def M1_MS : measure_space X := {
  to_measurable_space := M1,
  volume := μ_M1 }

#check M1_MS -- M1_MS : measure_space X

The above introduces a measure this way, which I have been trying to unpack today:

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
  (λ s _, finset.card s.to_finset)
  (by simp)
  (λ x h a, begin
    simp,
    sorry
  end)

In restricting the volume to [0,1] I am trying to get the Steinhaus probability space ([0,1], B([0,1]), μ) where μ is the volume restricted to [0,1]. I am still lost trying to understand the differences between

• abbreviation
• definition
• structure
• type class
• extends
• instance
  and what things get automatically defined, like to_X if you extend a class, and what you have to declare explicitly.

Thanks for your advice, I will keep trying to unroll the definitions until I get there.

[Lars Ericson]

"Steinhaus space" is a term I got from Stack Exchange. I think it is what is described here on page 36 and here on page 8.

[Lars Ericson]

The definition of measure_space contains some notation which is quite hard to parse. Looking at

structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
(m_Union ⦃f : ℕ → set α⦄ :
  (∀i, is_measurable (f i)) → pairwise (disjoint on f) →
  measure_of (⋃i, f i) = (∑'i, measure_of (f i)))
(trimmed : to_outer_measure.trim = to_outer_measure)

The notation m_Union ⦃f : ℕ → set α⦄ is hard to understand. The user's manual, section 4.9 seems to say (by omission) that the field names are just that: simple strings without type annotation. Section 3.3 on implicit arguments says that ⦃f : ℕ → set α⦄ is "an implicit argument, weakly inserted". It doesn't say what "weak insertion" means. The bound variable f is subsequently used in the (remainder of the) type of m_union, namely (∀i, is_measurable (f i)) → pairwise (disjoint on f) → measure_of (⋃i, f i) = (∑'i, measure_of (f i))). It is not clear if this is trying to say that the type of m_Union is say m_Union: Z where

Z = (Π ⦃f : ℕ → set α⦄ :  (∀i, is_measurable (f i)) → pairwise (disjoint on f) →  measure_of (⋃i, f i) = (∑'i, measure_of (f i)))

[Mario Carneiro]

In a structure field, (foo {x: A} : bla x) is the same as (foo : \all {x : A}, bla x)

[Bryan Gin-ge Chen]

"weak insertion" is explained in Section 6.5 of TPiL.

[Yury G. Kudryashov]

It seems that your A1 is equivalent to λ s, true.

[Yury G. Kudryashov]

And I think that this instance of measurable_space is called either \top or \bot (see what's used for naturals).

[Yury G. Kudryashov]

And the measure is called docs#measure_theory.measure.count

[Lars Ericson]

I am trying to unpack this:

import measure_theory.measure_space
import measure_theory.measurable_space

def X : Type := fin 3

def A1 : set X → Prop := λ a, a ∈ (𝒫 ⊤ : set (set X))

def M1 : measurable_space X := {
  is_measurable' := A1,
  is_measurable_empty := by {rw A1, finish},
  is_measurable_compl := assume a h, by {rw A1 at *, finish},
  is_measurable_Union := assume f hf, by {rw A1 at *, simp },
}

#check M1
instance XFT : fintype X := fin.fintype _
noncomputable instance amy (s : set X) : fintype s := by classical; apply_instance

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
  (λ s _, finset.card s.to_finset)
  (by simp)
  (λ x h a, begin simp, sorry end)

#check μ_M1 -- μ_M1 : measure_theory.measure X
#check μ_M1.m_Union -- ERROR

The last expression causes an error:

foobar.lean:26:0
failed to synthesize type class instance for
⊢ measurable_space X
foobar.lean:26:0
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ⁇
inferred
  M1

but the declaration of measure is:

structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
(m_Union ⦃f : ℕ → set α⦄ :
  (∀i, is_measurable (f i)) → pairwise (disjoint on f) →
  measure_of (⋃i, f i) = (∑'i, measure_of (f i)))
(trimmed : to_outer_measure.trim = to_outer_measure)

Also if I want to break out the actual measure as a separate function:

def actual_measure := λ s _, finset.card s.to_finset

but I don't understand how to break it out because I don't quite understand the arguments. I think s is of type ⦃f : ℕ → set α⦄. I'm not sure what the underscore is supposed to match, maybe (∀i, is_measurable (f i)) .

So 3 questions:

1. Is there any way to access the field m_Union, and what do you get if you do?

2. Is there any way to separately define actual_measure, and insert it like this:

noncomputable def μ_M1 : @measure_theory.measure X M1 :=
@measure_theory.measure.of_measurable _ M1
  (actual_measure)
  (by simp)
  (λ x h a, begin simp, sorry end)

3. Why does this cause Lean to go into an infinite loop:

#reduce μ_M1

P.S. I've had a very helpful realization when it comes to reading the code. I have been trying to "construct" objects like distance functions and measures and sigma algebras and so on. When I see what looks like an object in mathlib with a name like measure or measure_space, the grand realization is that this is, 99% of the time, a proof that that object's axioms hold. Sometimes but not always the object may hold something like m_Union which represents the thing that is being proven about. So, understanding that almost all objects in mathlib are proofs makes reading the code a lot easier (except for my questions above). I came to this realization by #reduce-ing the objects. However, attempting to #reduce some, like measure, causes Lean to loop.