Debut theorem and Doob-Meyer decomposition

Stream: Brownian motion

[Rémy Degenne]

@Lorenzo Luccioli @Alessio Rondelli @Pietro Monticone you added material about the Debut theorem (still in a PR) and the Doob-Meyer decomposition (that PR was merged). One proof in the Doob-Meyer part uses the Debut theorem, but actually it only uses it in a case of a hitting time indexed by a discrete set, so we could get that it's a stopping time by using the result specific to that case (which is already in Mathlib).
Is the Debut theorem also used elsewhere? I don't want to remove anything from the blueprint, I'm just asking in order to get a better understanding of how the various things you added relate to each other.

[Lorenzo Luccioli]

As you said, in the material that we added the Debut theorem is only used in discrete time.
In general, in the construction of the Stochastic Integral that we had in mind, it is used to show that the exit time of (the norm of) a process from [0, n] is a stopping time, but we don't have any blueprint material written about it at the time.

[Rémy Degenne]

Another remark about the Doob-Meyer proof in the blueprint: the processes M and A that are defined for the dyadics could be obtained from the Doob decomposition theorem that is already in Mathlib (in this file) in order to get some of their properties for free, but we would need to generalize the Mathlib code slightly: for now it's stated only for processes indexed by Nat, and we should generalize that type to a more general discrete (linearly ordered, etc) index.

That generalization is a self-contained task without prerequisites: if someone feels like opening a PR to Mathlib, that would be great!

[Rémy Degenne]

The generalization could be to a LinearOrder which is also a LocallyFiniteOrder and an OrderBot (there is an order iso from that to a subset of Nat; that file is related).

[Rémy Degenne]

WIP generalization of the Doob decomposition here: #31008

[Yongxi Lin (Aaron)]

I see that in the DoobMeyer file we have defined martingale part and predictable part of a local submartingale indexed by a general linearly ordered set. May I assume that the martingale part of a submartingale is indeed a martingale (in order to prove https://remydegenne.github.io/brownian-motion/blueprint/chap-filtration_martingale.html#lem:uniformIntegrable_stoppedValue_submartingale)?

[Rémy Degenne]

That lemma is about a process indexed by a discrete time, so you should use the discrete time Doob decomposition, in Mathlib: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Martingale/Centering.html#MeasureTheory.martingalePart.
It may be used somewhere in the proof of Doob-Meyer, so don't use the Doob-Meyer decomposition.

[Rémy Degenne]

I see the Lean statement has a generic countable index set, which does not correspond to what is used by that definition. Modify the Lean statement, probably?

[Rémy Degenne]

@Etienne Marion you added the Lean statement. What generality do you need downstream?

[Yongxi Lin (Aaron)]

It is certainly doable to use results in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Martingale/Centering.html#MeasureTheory.martingalePart to prove uniformIntegrable_stoppedValue_submartingale for processes indexed by $\mathbb{N}$, but I am just not sure what I should do if I need to prove it for a general linearly ordered set.

[Rémy Degenne]

Another option, without having checked whether it has a chance to work: try to follow the same proof as the martingale result, modifying an equality to an inequality somewhere? (I don't have time right now to check if that makes sense with that proof)

[Etienne Marion]

I copied down the hypotheses of the discrete optional sampling for martingales, but we only have Doob decompostion for Nat-indexed processes. As I said here I thought of adapting the proof for the martingale case as Rémy suggests, but it was suggested to use Doob-Meyer and I did not realize at the time that we would need a general index set so I went with that. I think it's a shame that we can't easily deduce results for discrete index from results about Nat though, to me that would be the best way to go in the long run.

[Rémy Degenne]

Well first we have to be careful about what we mean with "discrete index". For me it meant an index in which every point is isolated, basically a subset of Int. And my WIP refactor of the Doob decomposition mentioned above would work for those (or subsets of Nat perhaps). But you are talking about a countable linear order, which is more general.

[Etienne Marion]

Ah but I think I must have forgotten a LocallyFiniteOrder hypothesis then.

[Rémy Degenne]

So my suggestion in the other thread to use the Doob decomposition was for discrete in that sense. But for countable perhaps following the martingale proof is the best way. If we really nead the result for something more general than a subset of Nat, that is.

[Etienne Marion]

No I think we only need this for a subset of Nat, for the case where every point is isolated. The proof I had in mind for continuous time optional sampling for submartingales was to do the same as the one for martingales, which does require optional sampling in discrete time (in the sense of a subset of Nat, MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp). But as the proof of discrete time optional sampling was quite long I wondered if there wasn't an easier way which is why I opened #Brownian motion > Optional sampling for submartingales in the first place. Rémy if you think that #31008 would allow us to do that using only Doob-Meyer for Nat processes then I think it's the way to go. Otherwise we have to copy the proof of the martingale case.

[Rémy Degenne]

I'm tempted to use the copy and paste approach. Because it's doable without waiting for the refactor, and because it gives a more general result (which we might not really need, but that's still nice).
And in Lean copy-paste is fast.

[Rémy Degenne]

But I did not look at how much we would need to copy, so it might be underestimating it badly. I have to attend a seminar now so I'll come back to this discussion later.

[Etienne Marion]

Indeed copy paste is fast, although less nice :sweat_smile:, but it is probably the easier way indeed. Why do you think it would give a more general result? The hypotheses on $\iota$ in MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp are quite restrictive.

[Rémy Degenne]

My bad, I got confused.

[Etienne Marion]

I copied the martingale proof in #32204, it works like a charm!

[Etienne Marion]

Actually it looks like we have a problem, because if we do not assume that the index type satisfies LocallyFiniteOrderBot (which I think we don't want to because otherwise our approximations of stopping time must behave nicely and this should be painful) then we don't have integrability of the stopped value of a submartingale. But this can be solved if we assume that the submartingale is nonnegative. We need optional sampling of submartingales to show that nonnegative càdlàg submartingales are of class DL, so we can assume nonnegativity and things should work.

[Etienne Marion]

Well I can't get it to work... The proof of MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range does not work.

[Rémy Degenne]

Yes, I looked at it a bit and apparently when we downgrade all equalities to inequalities at that point one of them is the wrong way. Well... back to the Doob decomposition proof then! That means I have to actually finish that refactor. I was hoping not, because it's full of boring lemmas that I am duplicating from Nat to the more general "subset of Nat" order assumption list.

Unrelated remark: was that optional sampling file written before filter_upwards was available? (or perhaps simply before I became aware of it?) It's full of EventuallyEq.trans and other things I would never use any more.

[Etienne Marion]

I had a closer look at how @Kexing Ying formalized optional sampling in continuous time and I fear that the refactor might not be enough, because we don't want to assume LocallyFiniteOrder. I am not sure though, what do you think @Kexing Ying?

[Kexing Ying]

Sorry, I've not followed this conversation so I'm not sure if I understand the issue. Why does MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range not generalize to the submartingale case?

[Kexing Ying]

Rémy Degenne said:

Unrelated remark: was that optional sampling file written before filter_upwards was available? (or perhaps simply before I became aware of it?) It's full of EventuallyEq.trans and other things I would never use any more.

PS. it was after filter_upwards as indicated here

[Etienne Marion]

The proof uses a chain of equalities which become inequalities in the submartingale case, and those inequalities are not in the right direction.

[Kexing Ying]

Ah, I see... Is this the same case even for Nat indexed processes?

[Etienne Marion]

For Nat indexed processes we can prove the theorem directly using Doob's decomposition. In #31008 Rémy started a refactor to generalize this to an arbitrary index set which is a subset of Nat (in particular it is a locally finite order). But I am wondering if, in your proof of optional sampling in continuous time, having this hypothesis was fine. My feeling is that it's not the case since you don't want to have to check whether your approximations of stopping times have locally finite ranges?

[Kexing Ying]

Ah, I see. So the issue is that we can't necessarily have an order embedding from a countable set to a locally finite order.

[Etienne Marion]

I think so.

[Kexing Ying]

In that case, should we change the definition of DiscreteApproxSequence so that it requires that the range of the approximating stopping times to have an order embedding into Nat?

[Etienne Marion]

I guess one solution might be to ensure that the stopping times in an ApproximationSequence have locally finite range. I don't know if this would make the final result weaker or not.

[Etienne Marion]

Yes this seems a good idea.

[Kexing Ying]

Etienne Marion said:

I don't know if this would make the final result weaker or not.

As we need the time index to be a linear order anyway, I can't think of any candidates which are not "approximable" wrt the old definition but not with the new one

[Etienne Marion]

Yes I think even if there is a loss of generality (which is not clear at all) it won't be a problem.