Definition of a Gaussian process

Stream: Brownian motion

[Etienne Marion]

Etienne Marion said:

If nobody has claimed it I'll try lemma 3.32 IsGaussianProcess.modification.

I had to add an hypothesis to the lemma. I proved that a Gaussian process is almost everywhere measurable, so if Y is a modification of X and X is a Gaussian process, then Y might fail to be almost everywhere measurable (only if T is not countable), in which case it would not be a Gaussian process. Maybe we can change the definition of a Gaussian process to the following to avoid this?

def IsGaussianProcess (X : T → Ω → E) (P : Measure Ω := by volume_tac) : Prop :=
  ∀ I : Finset T, IsGaussian ((P.map (I.restrict ∘ fun ω t ↦ X t ω)))

Or

def IsGaussianProcess (X : T → Ω → E) (P : Measure Ω := by volume_tac) : Prop :=
  ∀ I : Finset T, IsGaussian ((P.map (fun ω ↦ I.restrict (X · ω))))

(which I find nicer).
In fact

def IsGaussianProcess (X : T → Ω → E) (P : Measure Ω := by volume_tac) : Prop :=
  ∀ I : Finset T, IsGaussian ((P.map (fun ω (i : I) ↦ X i ω)))

would be more consistent with the statement of finite_distributions_eq. Is there a reason why the latter uses a fintype rather than a finset?

[Notification Bot]

A message was moved here from #Brownian motion > Tasks and claims by Etienne Marion.

[Rémy Degenne]

Let's summarize the possible measurability conditions for X : T → Ω → E for T the index set and Ω the probability space (for my future reference as much as for anyone else).

For a measurable process, ∀ t, Measurable (X t) and Measurable (fun ω t ↦ X t ω) are equivalent by definition of the product measurable space.
If we want to relax to AEMeasurable, we can do it from either of these conditions, but ∀ t, AEMeasurable (X t) P and AEMeasurable (fun ω t ↦ X t ω) P are not equivalent anymore (unless T is countable). The first one is weaker.
The useful notion of a.e. measurable in any context is the one that corresponds to "almost everywhere equal to a measurable thing". Here the thing is a process, and that useful notion would be AEMeasurable (fun ω t ↦ X t ω) P. For the weaker condition, there may not be a single measurable process to which it's a.e. equal.

So I'm fine with having AEMeasurable (fun ω t ↦ X t ω) P as standard assumption everywhere. I used the weaker ∀ t, AEMeasurable (X t) P in several statements because at the start of the project I did not see that there was an issue.

[Rémy Degenne]

So I don't think the a.e.-measurability that the current definition of Gaussian process assumes is an issue, but there could be another good reason for changing the definition.

Your third def looks like a more natural way to describe the finite dimensional distributions than (P.map (fun ω t ↦ X t ω)).map I.restrict.

[Etienne Marion]

I agree this condition is not an issue. But indeed I think that it would be more natural to only do one mapping in the definition of a Gaussian process. Personally I prefer the second definition I wrote. The reason is that encoding the restriction into Finset.restrict rather than writing it with type ascription allows for more rewriting, for example to say that restricting to a finset I and then to a smaller one J (via Finset.restrict₂) is the same as directly restricting to J. Also, projective family of measures and projective limits are defined in terms of Finset.restrict₂ and Finset.restrict.
The only drawback I can see is that this would mean that when talking about finite dimensional distributions, we index them with a finset, and not an arbitrary finite type. I don't know if that is important or not.

[Rémy Degenne]

A PR to change the definition of a Gaussian process to your second definition would be welcome (or you can do it in your open PR about those processes).

[Rémy Degenne]

Related to the measurability discussion above, in https://github.com/RemyDegenne/brownian-motion/pull/104 I am changing the definition IsKolmogorovProcess to use something stronger (which I need for the Hölder modification lemmas). I am introducing a new definition for a measurable version of the condition, and IsKolmogorovProcess means being a.e. equal to a process that satisfies the measurable version.
The new definitions are:

structure IsMeasurableKolmogorovProcess (X : T → Ω → E) (P : Measure Ω) (p q : ℝ) (M : ℝ≥0) :
    Prop where
  measurablePair : ∀ s t : T, Measurable[_, borel (E × E)] (fun ω ↦ (X s ω, X t ω))
  kolmogorovCondition : ∀ s t : T, ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q

def IsKolmogorovProcess (X : T → Ω → E) (P : Measure Ω) (p q : ℝ) (M : ℝ≥0) : Prop :=
  ∃ Y, IsMeasurableKolmogorovProcess Y P p q M ∧ ∀ᵐ ω ∂P, ∀ t, X t ω = Y t ω

We should probably change the names later to IsKolmogorovProcess and IsAEKolmogorovProcess or something similar to fit better with the Mathlib names for Measurable/AEMeasurable, but I want to minimize the changes for now.

[Rémy Degenne]

@Etienne Marion a consequence of the change is that we should prove IsMeasurableKolmogorovProcess for the Brownian motion. Your code in https://github.com/RemyDegenne/brownian-motion/pull/105 should be easy to adapt.