Measure taking values in nat

Stream: new members

[Niclas Kupper]

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]

ℕ is a type, not a set, so n ∈ ℕ does not make sense. You want n : ℕ instead.

[Niclas Kupper]

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]

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]

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]

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]

And probably you want to take in a function set α → enat rather than merely assuming it exists.

[Yaël Dillies]

cc @Wrenna Robson for similar considerations in docs#hamming_dist

[Wrenna Robson]

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

[Wrenna Robson]

Is enat a complete linear order btw?

[Notification Bot]

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

[Yaël Dillies]

docs#enat.complete_linear_order

[Niclas Kupper]

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]

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

[Vincent Beffara]

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

[Yaël Dillies]

No, rather

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

[Yaël Dillies]

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]

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]

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

[Vincent Beffara]

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]

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

[Yaël Dillies]

I highly doubt you want the latter.

[Vincent Beffara]

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]

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]

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]

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]

I get no issue when I replace measure α with measure_theory.measure α

[Vincent Beffara]

(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]

thanks, my issue was that I was using a namespace but forgot the end at the end

[Niclas Kupper]

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]

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]

Don't call it measure_enat_of if it does not give you an enat :grinning_face_with_smiling_eyes:

[Niclas Kupper]

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]

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

[Vincent Beffara]

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]

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]

Thanks for all the help!

[Niclas Kupper]

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]

Niclas Kupper has marked this topic as unresolved.

[Niclas Kupper]

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