Zulip Chat Archive
Stream: Is there code for X?
Topic: Probability measure of B(R) and B([0,1])
Lars Ericson (Dec 07 2020 at 05:02):
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]) = ba
?
Yury G. Kudryashov (Dec 07 2020 at 16:01):
We already have the Lebesgue measure (available as the volume
on \R
).
Yury G. Kudryashov (Dec 07 2020 at 16:02):
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 (Dec 07 2020 at 16:59):
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 (Dec 07 2020 at 21:29):
We have docs#measure_theory.measure_space.volume
Yury G. Kudryashov (Dec 07 2020 at 21:30):
And docs#measure_theory.real.measure_space
Yury G. Kudryashov (Dec 07 2020 at 21:31):
So, if you write (volume : measure \R)
, then you get the Lebesgue meaure on \R
.
Yury G. Kudryashov (Dec 07 2020 at 21:32):
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 (Dec 07 2020 at 21:34):
You should define it using docs#measure_theory.measure.comap and coercion.
Lars Ericson (Dec 07 2020 at 22:11):
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, liketo_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 (Dec 07 2020 at 22:25):
"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 (Dec 07 2020 at 23:30):
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 (Dec 07 2020 at 23:32):
In a structure field, (foo {x: A} : bla x)
is the same as (foo : \all {x : A}, bla x)
Bryan Ginge Chen (Dec 07 2020 at 23:32):
"weak insertion" is explained in Section 6.5 of TPiL.
Yury G. Kudryashov (Dec 08 2020 at 02:47):
It seems that your A1
is equivalent to λ s, true
.
Yury G. Kudryashov (Dec 08 2020 at 02:48):
And I think that this instance of measurable_space
is called either \top
or \bot
(see what's used for naturals).
Yury G. Kudryashov (Dec 08 2020 at 02:50):
And the measure is called docs#measure_theory.measure.count
Lars Ericson (Dec 09 2020 at 02:59):
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:

Is there any way to access the field
m_Union
, and what do you get if you do? 
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)
 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.
Last updated: May 16 2021 at 05:21 UTC