Quadratic variation and Stietjes functions

Stream: Brownian motion

[Rémy Degenne]

In Mathlib, there is a definition docs#StieltjesFunction, which is a right-continuous monotone function from ℝ to ℝ. From such a function, we can get a measure StieltjesFunction.measure on ℝ. And the inverse operation of that is ProbabilityTheory.cdf.

In the project, we will define the predictable quadratic variation of a local martingale on some index set T satisfying some order/topology/measurability assumptions. The typical example is ℝ≥0.
The quadratic variation is a process with right-continuous monotone paths, so the paths are similar to Stieltjes functions but they are defined on T (for example ℝ≥0) instead of ℝ. For each one of those paths, we will want to get a measure to integrate against.

What I'm getting at is that we need to generalize docs#StieltjesFunction and docs#StieltjesFunction.measure to a class of domains that includes at least ℝ≥0.
We could perhaps generalize the code defining StieltjesFunction directly to a type satisfying a list of assumptions (to be defined), or alternatively assume that our index set T will always embed into ℝ and create a definition that goes to ℝ, gets a measure using the existing StieltjesFunction.measure, and maps it back to T.

Do you have thoughts on the best way to do that? Anybody wants to do it?

[Rémy Degenne]

Another consideration: we will also want to integrate against cadlag functions of locally bounded variation at some point, so we could focus on getting a signed measure out of those for index sets that include ℝ≥0, and then apply that mechanism to get a measure out of the quadratic variation.
With that option we don't need to spend time generalizing StieltjesFunction.

[Sébastien Gouëzel]

For me, the simplest way to get a measure from a (locally) bounded variation function is to write the function as a difference of two monotone functions (we already have that in mathlib) and then use the difference of the Stieltjes measures associated to the functions. So it would still be worth generalizing Stieltjes functions to more general index sets. Would conditionally complete linear orders be enough?

[Rémy Degenne]

Ah right, I forgot that we had that already. So going though monotone functions seems easier.
For the index set, ℝ≥0 and closed intervals of real numbers of the form [0,T] are my only examples for now, so yes, conditionally complete linear orders would definitely be enough.

[Rémy Degenne]

For reference: LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn
We will need a version of that result that takes a right-continuous function and returns two monotone right-continuous functions.

[Sébastien Gouëzel]

Rémy Degenne said:

Ah right, I forgot that we had that already. So going though monotone functions seems easier.
For the index set, ℝ≥0 and closed intervals of real numbers of the form [0,T] are my only examples for now, so yes, conditionally complete linear orders would definitely be enough.

ok, let me have a look.

[Rémy Degenne]

Sébastien Gouëzel generalized StieltjesFunction.measure to [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (this is now in Mathlib)