# Zulip Chat Archive

## Stream: new members

### Topic: Measure taking values in nat

#### Niclas Kupper (Oct 14 2022 at 13:37):

Hi, I'm new to Lean and trying to learn more by implementing point processes. I'm already stuck on the first definition. I want to create a new structure for measures that only take values in `\nat`

and I am unsure why my approach doesn't work

```
structure finite_point_measure (α : Type*) [measurable_space α] extends measure α :=
(in_nats (A : set α) (measurable_set A) :
∃ n ∈ ℕ, measure_of A = n)
```

any help would be appreciated. If this is the wrong place to ask please just point me in the right direction. thanks~

#### Yaël Dillies (Oct 14 2022 at 13:39):

`ℕ`

is a **type**, not a **set**, so `n ∈ ℕ`

does not make sense. You want `n : ℕ`

instead.

#### Niclas Kupper (Oct 14 2022 at 13:43):

Thanks, that is already helpful, sadly that did not fix the error yet. I'll play around a bit more and come back if I still can't fix it

#### Riccardo Brasca (Oct 14 2022 at 13:45):

In any case try to post #mwe (including the imports and so on, the idea is that we can copy/paste your code and see what happens). Note that `measure`

refers to docs#measure, that is probably not what you want.

Finally, it's probably a good idea to open a new conversation in the "new members" stream. I can move your message if you want.

#### Niclas Kupper (Oct 14 2022 at 13:48):

Yes, thanks, will keep in mind in the future. I got it working now. Yes, you can move this to the new members stream, didn't see it earlier

#### Vincent Beffara (Oct 14 2022 at 13:52):

Also, you might want your measure to take values in docs#enat instead, since many (most?) point processes used in practice are only locally finite

#### Yaël Dillies (Oct 14 2022 at 13:56):

And probably you want to take in a function `set α → enat`

rather than merely assuming it exists.

#### Yaël Dillies (Oct 14 2022 at 13:56):

cc @Wrenna Robson for similar considerations in docs#hamming_dist

#### Wrenna Robson (Oct 14 2022 at 13:57):

Hmm is this the mythical second example! I guess it's a measure not a metric.

#### Wrenna Robson (Oct 14 2022 at 13:59):

Is enat a complete linear order btw?

#### Notification Bot (Oct 14 2022 at 13:59):

10 messages were moved here from #general > measure theory by Riccardo Brasca.

#### Yaël Dillies (Oct 14 2022 at 14:00):

docs#enat.complete_linear_order

#### Niclas Kupper (Oct 14 2022 at 16:06):

Yaël Dillies said:

And probably you want to take in a function

`set α → enat`

rather than merely assuming it exists.

I tried to do that, but I wasn't just able to overwrite the `measure_of`

function. If there is a way to do it i'd be happy to implement it that way

#### Yaël Dillies (Oct 14 2022 at 16:08):

No, don't overwrite it. Simply state that they are compatible.

#### Vincent Beffara (Oct 14 2022 at 16:15):

You mean `{ \mu : measure \alpha // \exists f : set \alpha \to enat, \forall s, measurable s -> \mu s = f s }`

?

#### Yaël Dillies (Oct 14 2022 at 16:17):

No, rather

```
(measure_enat_of : set α → enat)
(coe_measure_enat_of : ∀ s, measurable s → ↑(measure_enat_of s) = measure_of s)
```

#### Yaël Dillies (Oct 14 2022 at 16:18):

Or even

```
(measure_enat_of : set α → enat)
(coe_measure_enat_of : ∀ s, ↑(measure_enat_of s) = measure_of s)
```

because I think the junk value for `measure_of`

will make it work out.

#### Vincent Beffara (Oct 14 2022 at 16:27):

What would be the difference in practice between `\exists f : set \alpha \to enat, \forall s : set \alpha, ...`

and `\forall s : set \alpha, \exists n : enat, ...`

? Those feel pretty isomorphic to each other. And if you have either, then `measure_enat_of`

can be derived from `measure_of`

.

#### Yaël Dillies (Oct 14 2022 at 16:29):

Well, you have to use choice every time you want to use one, while you can readily use the other.

#### Vincent Beffara (Oct 14 2022 at 20:40):

While I'm asking: would another option be to define a typeclass `[is_int_valued_measure \mu]`

instead of a new type for int-valued measures?

#### Yaël Dillies (Oct 14 2022 at 21:05):

The question is whether you want to have an int-valued measure or merely know that there exists one.

#### Yaël Dillies (Oct 14 2022 at 21:05):

I highly doubt you want the latter.

#### Vincent Beffara (Oct 14 2022 at 21:11):

I would say that you want a plain old measure but know that it actually takes values in the integers. Something like this (but less clumsy):

```
variables {α β : Type*}
class has_values_of_type (f : α → β) (γ : Type*) [has_coe γ β] :=
(to_fun : α → γ)
(eq : ∀ a : α, f a = ↑(to_fun a))
instance coe_enat_ennreal : has_coe enat ennreal :=
by { refine ⟨λ n, _⟩, refine n.cases_on ⊤ (λ n', _), exact some n' }
class is_integer_valued [measurable_space α] (μ : measure_theory.measure α) :=
(toto : has_values_of_type μ enat)
example [measurable_space α] {μ : measure_theory.measure α} [is_integer_valued μ] :
∃ n : enat, μ set.univ = n :=
by simp only [is_integer_valued.toto.eq, exists_apply_eq_apply']
```

#### Yaël Dillies (Oct 14 2022 at 21:23):

Still, why not just state the commutative diagram rather than its mere existence in an inconvenient form? Like, do you *really* not want to access the `enat`

-valued function?

#### Vincent Beffara (Oct 14 2022 at 21:40):

In fact I don't know, it is not at all clear to me... but I think I would like to treat an int-valued measure as much like a usual measure for as long as possible, and only use the information that it is int-valued inside a few key lemmas, so a typeclass feels more natural. In my head, `[is_integer_valued \mu]`

and `[is_probability_measure \mu]`

have the same status; that one of them can be implemented as a `set \alpha \to enat`

feels incidental.

Besides, I still kind of followed your suggestion, the function is right there as `has_values_of_type.to_fun`

if you need it :wink:

#### Niclas Kupper (Oct 18 2022 at 13:22):

Okay, so I have now tried to define a point measure as a sum of finite point measures and I am still running into problems. Lean seems to be complaining about my `sum_of_measures`

condition, but I'm not sure why. Any help is appreciated, thanks!

```
import measure_theory.measurable_space_def
import measure_theory.measurable_space
import measure_theory.measure.measure_space_def
import data.real.basic
import data.nat.cast.defs
structure finite_point_measure (α : Type*) [measurable_space α] extends measure α :=
(measure_enat_of : set α → ℕ)
(coe_measure_enat_of : ∀ s, ↑(measure_enat_of s) = measure_of s)
structure point_measure (α : Type*) [measurable_space α] extends measure α :=
(fin_point_measures : ℕ → finite_point_measure α)
(sum_of_measures : ∀ s, measure_of s = ∑'i, (fin_point_measures i).measure_enat_of s)
```

#### Vincent Beffara (Oct 18 2022 at 13:35):

I get no issue when I replace `measure α`

with `measure_theory.measure α`

#### Vincent Beffara (Oct 18 2022 at 13:37):

(Well, I do have a mathematical issue which is that you are not storing the sum but really an indexed family of finite point measures, but two such decompositions giving the same sum should probably be identical.)

#### Niclas Kupper (Oct 18 2022 at 13:40):

thanks, my issue was that I was using a `namespace`

but forgot the `end`

at the end

#### Niclas Kupper (Oct 18 2022 at 13:41):

How would you store the sum directly? I guess for my definition to be correct I would have to make some sort of equivalence class?

#### Vincent Beffara (Oct 18 2022 at 13:52):

I would avoid going down this road of defining equivalence relations for this. Rather, I would do

```
import data.nat.enat
import measure_theory.measurable_space
instance with_top.has_coe_t' {α β : Type*} [has_coe_t α β] : has_coe_t (with_top α) (with_top β) :=
⟨with_top.map has_coe_t.coe⟩
instance : has_coe_t ℕ∞ ennreal := with_top.has_coe_t'
structure point_measure (α : Type*) [measurable_space α] extends measure_theory.measure α :=
(measure_enat_of : set α → enat)
(coe_measure_enat_of : ∀ s, measure_of s = measure_enat_of s)
```

(where the first two `coe`

instances are probably somewhere in mathlib already but I couldn't find them)

#### Vincent Beffara (Oct 18 2022 at 13:53):

Don't call it `measure_enat_of`

if it does not give you an `enat`

:grinning_face_with_smiling_eyes:

#### Niclas Kupper (Oct 18 2022 at 16:00):

Thanks! If I now want to build the measurable space of point measures (where the sigma-algebra is generated by sets

` ∀B∀k {η(B)=k}`

where would I even begin? Should I implement that as an instance or a def. Also I'm not sure how to write sets of sets I guess.

#### Vincent Beffara (Oct 18 2022 at 19:55):

You can have a look at docs#measurable_space.generate_measurable and docs#measurable_space.generate_from

#### Vincent Beffara (Oct 18 2022 at 20:02):

Maybe something like this,

```
def elementary (B : set α) (k : enat) : set (point_measure α) :=
{μ | μ.measure_enat_of B = k}
def elementaries (α : Type*) [measurable_space α] : set (set (point_measure α)) :=
{S | ∃ B k, measurable_set B ∧ S = elementary B k}
instance : measurable_space (point_measure α) :=
measurable_space.generate_from (elementaries α)
```

but there has to be a better way of defining `elementaries`

.

#### Niclas Kupper (Oct 18 2022 at 20:19):

Vincent Beffara said:

You can have a look at docs#measurable_space.generate_measurable and docs#measurable_space.generate_from

I tried this, but I wasn't quite able to get it to work

#### Niclas Kupper (Oct 18 2022 at 20:19):

Thanks for all the help!

#### Niclas Kupper (Oct 20 2022 at 14:01):

Hi, I'm trying to define a Poission random variable and am starting by defining the pmf, but I'm having problems with casting between `nat`

and `real`

and `nnreal`

. Also is this the right approach? thanks!

```
def poission_pmf (l : ℝ≥0) (k : ℕ) : ℝ≥0 :=
(real.exp (-l) * l^k) / (nat.factorial k)
```

EDIT:

nevermind: figured it out

```
def poission_pmf (l : ℝ≥0) (k : ℕ) : ℝ≥0 :=
((real.to_nnreal (real.exp(-l)) * l^k : ℝ≥0) / (nat.factorial k : ℝ≥0))
```

#### Notification Bot (Oct 20 2022 at 19:37):

Niclas Kupper has marked this topic as unresolved.

#### Niclas Kupper (Oct 20 2022 at 19:39):

That might be a good idea, I'll try that tomorrow – still not that comfortable with writing proofs in lean, so I might try proving basic facts about Poission RVs first

Last updated: Dec 20 2023 at 11:08 UTC