Stream: General

Topic: Repeated integral for ordered indices

Christian Pardillo Laursen (Jul 29 2025 at 21:36):

I'm trying to construct Brownian motion, and part of this involves defining a projective family: given some index set I :: real set, we need to construct a measure $\nu$ with type "(real => real) measure" that is well-behaved under projection (term projective_family in Probability/Projective_Family.thy).

For the Brownian motion construction I'm following (Øksendal), we assume our set can be arranged into terms

$$0 \leq t_1 < t_2 < \dots < t_k$$

Then, we can define the measure as follows, writing p(σ, μ, x)\) for the normal density:

$$\nu_{t_1, \dots, t_k}(F_1 \times \dots \times F_k) = \int_{F_1 \times \dots \times F_k} p(t_1, x, x_1) \dots p(t_k - t_{k-1}, x_{k-1}, x_k)dx_1\dots dx_k$$

I'm thinking of doing this by first getting a sorted list from the index set, and then constructing the integral as a primrec. Does this sound reasonable? Is there a better way? As far as I can tell, nobody has ever constructed a projective family in Isabelle so I don't have anything to go off.

Manuel Eberl (Aug 04 2025 at 12:47):

I'm not fully sure I understand what you're doing here (what are the $F_i$, for example), but the normal way to do a "multi-dimensional" integral is to use product measures.

This is done by the PiM operator:

term "Π⇩M x∈I. M"
"Pi⇩M I (λx. M)" :: "('a ⇒ 'b) measure"

There are all the obvious lemmas about Π⇩M x∈{y}. M x and Π⇩M x∈I∪J. M x that allow you to work with this. Your approach with the list and the primrec works as well, of course (at least for a finite number of dimensions) but things will probably become messy as soon as you want to change the order of things or pull out a dimension other than the first one.

There are some examples of this in the distribution and the AFP:

• Density Compiler: This entry describes a compiler that compiles from a functional probabilistic programming language into probability density functions. This requires integrating over all variables occurring in the context, which of course results in a lot of manipulation of indexed integrals like the one you describe. It gets a bit messy, of course.
• Ball_Volume: This derives the formula for the volume of a unit ball in n-dimensional Euclidean space by repeated integration. Basically, it's an induction on the dimension n: the n-dimensional integral is pulled apart into an (n-1)-dimensional integral with a 1-dimensional integral inside.

Hope that helps!

Last updated: Aug 23 2025 at 01:39 UTC