measure theory

Stream: new members

[Brandon Brown]

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]

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

[Brandon Brown]

oh of course, good catch, thanks

[Alex J. Best]

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]

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

[Brandon Brown]

ah I just need to import topology.instances.ennreal

[Brandon Brown]

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]

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

[Yury G. Kudryashov]

Here ⋃₀ is set.sUnion.

[Brandon Brown]

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

[Yury G. Kudryashov]

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]

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]

or should I just use ennreal.​to_real ?

[Alex J. Best]

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]

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]

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]

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

[Pedro Minicz]

That would guarantee that to_real is always well behaved.

[Pedro Minicz]

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

[Brandon Brown]

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

[Brandon Brown]

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

[Brandon Brown]

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

[Pedro Minicz]

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]

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

[Pedro Minicz]

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

[Pedro Minicz]

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]

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

[Brandon Brown]

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

[Pedro Minicz]

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]

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.