## 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: May 11 2021 at 14:11 UTC