Need some advice on structuring type classes

Stream: mathlib4

[Björn Wehlin]

I'm making an attempt at formalizing point processes as random measures. However, I'm having some difficulty coming up with a good class structure for this.

Essentially, I would like to have a class PointProcess (or structure?) that consists of

• a random variable Ω → Measure E where Ω and E are measurable spaces, and there is a probability measure μ defined Ω.
• a property that the random variable fulfills a property IsPointMeasure (defined elsewhere) almost surely.

To showcase how I'm trying to use PointProcess instances, I have attempted to define a function evaluation_map (hopefully it's clear from what's in the code what I'm trying to do)

My first attempt:

variable {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
variable {μ : Measure Ω} [IsProbabilityMeasure μ]

class PointProcess where
  rv : Ω → Measure E
  is_point_measure_as : μ {ω | IsPointMeasure (rv ω)} = 1

def evaluation_map (N : PointProcess) (a : Set E) : Ω → EReal := (fun ν => ν a) ∘ N.rv

This gives an error

typeclass instance problem is stuck, it is often due to metavariables
  MeasurableSpace ?m.503

on evaluation_map.

I've tried adding the following:
class PointProcess (Ω E : Type*) [MeasurableSpace Ω] [MeasurableSpace E] (μ : Measure Ω) [IsProbabilityMeasure μ] where
but it seems I have to keep parameterizing things on Ω E μ and adding [MeasurableSpace Ω] etc.

I would like to end up with something where some version of this makes sense:

def IsStationary (N : Type*) [PointProcess N] : Prop := -- some more things are needed here to make mathematical sense
  sorry

Maybe there are more questions that answers from what I've asked here, and I realize I'm not being super precise, but any advice is welcome. I'm happy to clarify things as needed.

[Notification Bot]

This topic was moved here from #lean4 > Need some advice on structuring type classes by Kyle Miller.

[Kyle Miller]

Could you give a #mwe? I got about to here before noticing that IsPointMeasure is probably your definition.

import Mathlib

open MeasureTheory

variable {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
variable {μ : Measure Ω} [IsProbabilityMeasure μ]

class PointProcess where
  rv : Ω → Measure E
  is_point_measure_as : μ {ω | IsPointMeasure (rv ω)} = 1

def evaluation_map (N : PointProcess) (a : Set E) : Ω → EReal := (fun ν => ν a) ∘ N.rv

(Having an mwes helps people spend their time answering questions rather than multiple people potentially duplicating this preparatory work. A good guideline is that if you see an error, the mwe should have the error too.)

[Björn Wehlin]

Hi, sorry, yes, I realize it's not the best question. Part of the problem is the w in mwe :)

Yes, IsPointMeasure is my definition. Here's a reworked version without it:

import Mathlib

open MeasureTheory

variable {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
variable {μ : Measure Ω} [IsProbabilityMeasure μ]

def IsLessThanFive (ν : Measure E) : Prop := ∀ s : Set E, ν s < 5

class PointProcess (Ω E : Type*) [MeasurableSpace Ω] [MeasurableSpace E]
    (μ : Measure Ω) [IsProbabilityMeasure μ]  where
  rv : Ω → Measure E
  is_point_measure_as : μ {ω | IsLessThanFive (rv ω)} = 1

theorem test234 {N : PointProcess Ω E μ} : False := by
  sorry

This finally compiles but now I'm having issues with declaring things as instances of PointProcess (obviously ℝ does not satisfy being a PointProcess -- I just used ℝ since it's a readily available type):

-- function expected at
--    PointProcess Ω E μ
--  term has type
--    Type (max u_1 u_2)
instance : (PointProcess Ω E μ) ℝ where
  rv := sorry
  is_point_measure_as := sorry

[Etienne Marion]

As the error message says, you are applying PointProcess Ω E μ to ℝ as though PointProcess Ω E μ is some kind of predicate which takes an object as input and outputs whether or not it satisfies the property, but it is not what it is. That's what function expected means. If you want a predicate on random variables then you can just use IsPointMeasure.

[Rémy Degenne]

I'll let others help you with your specific questions, but I just want to point out that Mathlib has a class ProbabilityTheory.Kernel for measurable maps from a measurable space to the measures on another space, and you probably want to use it:

import Mathlib
open MeasureTheory ProbabilityTheory

variable {Ω E : Type*} {mΩ : MeasurableSpace Ω} {mE : MeasurableSpace E}

/-- This is a possible way to express the property of being a point process. -/
class IsPointProcess (κ : Kernel Ω E) (μ : Measure Ω) : Prop where
  IsNat : ∀ᵐ ω ∂μ, ∀ s, ∃ n : ℕ, κ ω s = n

-- use it like this
example (κ : Kernel Ω E) (μ : Measure Ω) [IsPointProcess κ μ] : 0 = 0 := rfl

[Björn Wehlin]

Etienne Marion said:

As the error message says, you are applying PointProcess Ω E μ to ℝ as though PointProcess Ω E μ is some kind of predicate which takes an object as input and outputs whether or not it satisfies the property, but it is not what it is. That's what function expected means. If you want a predicate on random variables then you can just use IsPointMeasure.

It's a bit too strong to require that IsPointMeasure holds for the random variable -- I want to require it only almost surely.

I suppose, however, I could do something like this: def IsPointProcess (N : Ω → Measure E) : Prop := μ {ω | IsLessThanFive (N ω)} = 1 but with IsPointMeasure rather than IsLessThanFive. Maybe introducing classes here is too heavy-handed to begin with.

[Rémy Degenne]

The ∀ᵐ ω ∂μ, ... piece of code in my message above states that something holds almost surely

[Björn Wehlin]

Thanks, @Rémy Degenne, this looks like a more canonical way to accomplish what I'm trying to do.

[Etienne Marion]

If you only need a predicate then indeed a class is probably not necessary, a simple def will suffice. Also it's better to use structure rather than class if you don't need to use typeclass inference.

[Björn Wehlin]

Thanks. It's still a bit unclear to me in this case whether I'll want typeclass inference or not (hopefully it'll become clear as I build things out).