Right continuous process

Stream: Brownian motion

[Kexing Ying]

Whenever we say right continuous process, do we mean the process is a.s. right continuous (i.e. indistinguishably right continuous) or its bona fide right continuous? I ask this because, for the continuous time optional sampling theorem I think I need the process to be progressively measurable which I think is not necessarily true for a.s. right continuous processes (as the Borel sigma algebra is not complete).

[Etienne Marion]

You are right the uncompleteness of the Borel sigma algebra will cause some issue. Maybe you could do something similar to what we do with independence. First prove something in the case with stronger hypotheses (here right-continuous everywhere) and then in the case where X is only almost surely right continuous, introduce an undistinguishable process Y which is right-continuous everywhere on which you can apply the previous result, and conclude using the fact the property you are proving is closed under undistinguishability.

[Yongxi Lin (Aaron)]

I am trying to prove that a right continuous adapted process X : ι → Ω → β is progressively measurable. Should I just prove this in the case that ι = [0,∞) or find the most general assumptions on ι so that a discrete approximation of X can be constructed?

[Etienne Marion]

I think something involving DenselyOrdered should work?

[Yongxi Lin (Aaron)]

I see. Maybe that why the current problem statement assume ι has a SecondCountableTopology? Suppose it has a countable dense set $u : ℕ → (-∞, t]$, where t : ι. For each $n\in \mathbb{N}$, I can rearrange the first $n$ elements so that they are in an increasing order. I'll denote these elements in increasing order by $v_1 \le v_2 \le \cdots \le v_n$ to avoid any confusion ($\{v_1,\cdots, v_n\}= \{u_1, \cdots, u_n\}$). Define the discrete approximation as

$X^n_s=X^n_{v_{i + 1}}$ if $s\in (v_i, v_{i+1}]$

(where $v_{n+1}:=t$).

[Etienne Marion]

@Kexing Ying do you know how the proof works with the hypotheses which are in the lean file?

[Kexing Ying]

Yes, I think you need DenselyOrdered for this

[Etienne Marion]

Ok si I think your idea is right Aaron. If you assume DenselyOrdered then any point of ι will be approximated from above by your dense sequence, so taking approximating the identity of ι by s n which maps i : ι to its nearest neighbor on the right among the first n terms should give you a sequence of simple functions which converges to the identity from above, which is what you want.

[Etienne Marion]

You will most certainly have to assume OrderTopology. It will work because if your dense sequence does not approximate any point from above, then you will have one point which has a right neighborhood not intersecting the sequence, but this neighborhood will contain points which won't be approximated by your sequence at all contradicting its density. I think the metrizable assumption won't be necessary (but complete the proof before weakening hypotheses!), maybe it was put there to match those of MeasureTheory.stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable which is similar. But here the fact that we have a nice order is probably enough.

[Sébastien Gouëzel]

I'm not sure you should assume DenselyOrdered. For instance, isn't it true also in the naturals? If you assume just that you have a linear order which is second countable for its order topology, then the set of points which are isolated on the right is countable (we have that in mathlib), so taking as your countable set a dense set union the sets of points which are isolated on the right, I hope everything would work.

[Yongxi Lin (Aaron)]

Thank for these helpful suggestions. I'll try to prove this without the DenselyOrdered assumption. Before I proceed, I have another question about the discrete approximation. What is the canonical way of defining a piecewise function in lean? My plan is to use IndexedPartition.piecewise and then prove the following lemma:

import Mathlib

open MeasureTheory

variable {ι Ω β : Type*} [TopologicalSpace β] {mΩ : MeasurableSpace Ω} {X : ι → Ω → β}

lemma _root_.MeasureTheory.StronglyMeasurable.IndexedPartition {s : ι → Set Ω} [Countable ι]
    (hs : IndexedPartition s) (hm : ∀ i, MeasurableSet (s i))
    (hX : ∀ i, StronglyMeasurable (X i)):
    StronglyMeasurable (hs.piecewise X) := by sorry

which is an analogue of MeasureTheory.StronglyMeasurable.piecewise

[Etienne Marion]

I didn't know about IndexedPartition.piecewise so I don't know how convenient it is to work with, but this looks like a reasonable approach.

[Kexing Ying]

Currently I don't think https://remydegenne.github.io/brownian-motion/blueprint/sect0004.html#lem:stable_IsMartingale is true since we don't assume right continuity. Should we assume right continuity in the definition of local martingale so that local martingale is a stable property?

[Etienne Marion]

I think it would make sense yes, non-càdlàg martingales are not very interesting anyway I think.

[Kexing Ying]

Btw, do you know when we will need the làg part of càdlàg. I think we've so far only needed right continuity

[Etienne Marion]

I needed it to prove that $\inf \{t | |X_t| \ge n\}$ is a localizing sequence. It is needed here because a càdlàg function is bounded on compact sets, which is not true if you only assume right-continuity. I think this localizing sequence is a key fact when building the stochastic integral so it will certainly become essential in this part of the blueprint.

[Rémy Degenne]

Kexing Ying said:

Currently I don't think https://remydegenne.github.io/brownian-motion/blueprint/sect0004.html#lem:stable_IsMartingale is true since we don't assume right continuity. Should we assume right continuity in the definition of local martingale so that local martingale is a stable property?

Yes, I think we should add cadlag in the definition of IsLocalMartingale, because that's the object with nice properties. We can use Locally (Martingale · 𝓕 P) 𝓕 X P to talk about the current definition (notably when we will show that every local martingale, in the non cadlag sense, has a cadlag local martingale modification). This page follows that convention and defines: "a process is a local martingale if it is locally in the class of cadlag martingales".

[Rémy Degenne]

Oh I just realized that there is a difference there between two possible definitions that use cadlag: cadlag and locally martingale, vs locally both cadlag and martingale.

[Rémy Degenne]

And presumably Lowther chooses the second one for a good reason (it's the local property of the interesting class of cadlag martingales), and the stability properties we want are about cadlag (sub)martingales.