Zulip Chat Archive

Stream: new members

Topic: measure theory


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)))

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.

Brandon Brown (Aug 14 2020 at 02:30):

oh of course, good catch, thanks

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.

Brandon Brown (Aug 14 2020 at 02:35):

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

Brandon Brown (Aug 14 2020 at 02:43):

ah I just need to import topology.instances.ennreal

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)

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)

Yury G. Kudryashov (Aug 14 2020 at 05:25):

Here ⋃₀ is set.sUnion.

Brandon Brown (Aug 14 2020 at 12:54):

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

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.

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?

Brandon Brown (Aug 15 2020 at 02:14):

or should I just use ennreal.​to_real ?

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

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)

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)

Pedro Minicz (Aug 15 2020 at 02:20):

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

Pedro Minicz (Aug 15 2020 at 02:20):

That would guarantee that to_real is always well behaved.

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.

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

Brandon Brown (Aug 15 2020 at 02:24):

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

Brandon Brown (Aug 15 2020 at 02:25):

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

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)  σ)

Pedro Minicz (Aug 15 2020 at 02:27):

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

Pedro Minicz (Aug 15 2020 at 02:27):

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

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:

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.

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

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:

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: Dec 20 2023 at 11:08 UTC