Zulip Chat Archive

Stream: new members

Topic: measure theory


view this post on Zulip Brandon Brown (Aug 14 2020 at 02:09):

This is more of a mathematics question as the following code type checks. As a self-learner, hoping someone could help verify my definition of a measure space is mathematically correct.

import data.set.basic
import data.set.disjointed
import data.set.countable
import data.real.basic
import topology.algebra.infinite_sum
import tactic
open_locale big_operators
open set

universe u

class measurable_space (Ω : Type u) :=
(σ : set (set Ω))
( nonempty : set.nonempty σ)
( closed_complements :  s  σ, s  σ)
( closed_unions :  f :   set Ω, ( i : , (f i)  σ)  ( i, f i)  σ)

structure measure' {Ω : Type u}
(S : measurable_space Ω) :=
(μ : set Ω  )
(nonnegative :  s  S.σ, μ s  0)
(null_is_zero : μ  = 0)
(countable_additivity :  f :   set Ω,  i k, i  k  f i  f k =   μ ( i, f i) = (∑' i, μ (f i)))

view this post on Zulip Alex J. Best (Aug 14 2020 at 02:27):

I think for countable additivity you would want to assume that all f i are measurable for that to hold.

view this post on Zulip Brandon Brown (Aug 14 2020 at 02:30):

oh of course, good catch, thanks

view this post on Zulip Alex J. Best (Aug 14 2020 at 02:31):

I also think you would want the measure to be valued in ennreal which includes infinity, as there are measurable sets which have infinite measure.

view this post on Zulip Brandon Brown (Aug 14 2020 at 02:35):

right. hmm when I use ennreal then ∑' stops working

view this post on Zulip Brandon Brown (Aug 14 2020 at 02:43):

ah I just need to import topology.instances.ennreal

view this post on Zulip Brandon Brown (Aug 14 2020 at 03:26):

import data.set.basic
import data.set.disjointed
import data.set.countable
import data.real.basic
import data.real.ennreal
import topology.algebra.infinite_sum
import topology.instances.ennreal
import tactic
open_locale big_operators
open set

universe u

structure measurable_space (Ω : Type u) :=
(σ : set (set Ω))
( nonempty : set.nonempty σ)
( closed_complements :  s  σ, s  σ)
( closed_unions :  f :   set Ω, ( i : , (f i)  σ)  ( i, f i)  σ)

structure measure_space (Ω : Type u) extends measurable_space Ω :=
(μ : set Ω  ennreal)
(null_is_zero : μ  = 0)
(countable_additivity :  f :   set Ω,  i k, f i  σ  i  k  f i  f k =   μ ( i, f i) = (∑' i, μ (f i)))

structure probability_space (Ω : Type u) extends measure_space Ω :=
(unitarity : μ univ = 1)

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 05:24):

Another way to formulate the same assumption is ∀ S : set (set α), countable S → (∀ s ∈ S, is_measurable s) → is_measurable (⋃₀ S)

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 05:25):

Here ⋃₀ is set.sUnion.

view this post on Zulip Brandon Brown (Aug 14 2020 at 12:54):

that is certainly more concise than what I have, thanks for the alternative

view this post on Zulip Yury G. Kudryashov (Aug 14 2020 at 16:39):

As far as I understand, the definition in mathlib uses families enumerated by natural numbers because it's easier to prove this for a given function is_measurable. The lemma is_measurable.sUnion says what I wrote above.

view this post on Zulip Brandon Brown (Aug 15 2020 at 00:52):

I'm trying to use the ring tactic to re-arrange an equation involving measures on measurable sets, e.g. show that P.μ B = (P.μ A) + (P.μ (B \ A)) is the same as (P.μ A) = (P.μ B) - (P.μ (B \ A)) where P.μ is a measure and A B are measurable sets. The ring tactic isn't working. The measure sends measurable sets to ennreal which is a commutative semiring so shouldn't the ring tactic work? Or is it because P.μ B is not a single term so it can't re-write it?

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:14):

or should I just use ennreal.​to_real ?

view this post on Zulip Alex J. Best (Aug 15 2020 at 02:18):

I guess the answer might depend on what your goals are, do you really need real values, for some arithmetic and stuff? to_real should work fine. Probably its cleanest to define define def probability_space.prob_μ [probability_space \Omega] : set \Omega \to \R := sorry

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:18):

You could go for the mathlib definition of probability measure:

/-- A measure `μ` is called a probability measure if `μ univ = 1`. -/
class probability_measure (μ : measure α) : Prop := (meas_univ : μ univ = 1)

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:19):

that's what I have I think

structure measure_space (Ω : Type u) extends measurable_space Ω :=
(μ : set Ω  ennreal)
(null_is_zero : μ  = 0)
(countable_additivity :  f :   set Ω,  i k, f i  σ  i  k  f i  f k =   μ ( i, f i) = (∑' i, μ (f i)))

structure probability_space (Ω : Type u) extends measure_space Ω :=
(unitarity : μ univ = 1)

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:20):

It implies that for any set s in the σ-algebra μ s ≤ 1.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:20):

That would guarantee that to_real is always well behaved.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:21):

However, note that your definition of measurable_space is not quite a σ-algebra, so it might not work as expected.

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:22):

I'm trying to prove monotonicity and I think I need real values to use ring operations for the proof

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:24):

@Pedro Minicz oh what am I missing? That property that Ω is the universal set?

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:25):

(I have no formal math background beyond calculus, please forgive my naïveté )

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:26):

The universe set for the type Ω should be in the σ-algebra.

structure measurable_space (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_unions :  f :   set Ω, ( i : , (f i)  σ)  ( i, f i)  σ)

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:27):

I replaced nonempty because set.univ ∈ σ → set.nonempty σ.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:27):

It feels like its what you wanted to be there in the first place.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:28):

Also, don't worry, I am a CS guy who just got deep into maths recently, we are all learning. :grinning_face_with_smiling_eyes:

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:30):

thanks! I definitely wouldn't have wanted to start to prove things when it wasn't quite a sigma algebra.

view this post on Zulip Brandon Brown (Aug 15 2020 at 02:30):

And cool! glad I'm not the only one. Lean is basically the reason I'm motivated to learn math

view this post on Zulip Pedro Minicz (Aug 15 2020 at 02:35):

The rabbit hole is deep. Proof assistants got me into math a year ago... no end in sight, and that is awesome! Welcome! :octopus:

view this post on Zulip Alex J. Best (Aug 15 2020 at 03:34):

I think nonempty is equivalent to the univ being a member right? If the measurable sets are nonempty we have a measurable set and so its complement is measurable also, so the union of these two is also measurable.


Last updated: May 11 2021 at 14:11 UTC