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