Itô’s Lemma

Stream: Is there code for X?

[Pietro Monticone]

Has the Itô’s lemma been formalized and included in Mathlib?

[Yaël Dillies]

No, but @Jason KY. is working on prerequisites

[Kexing Ying]

FYI I've not written much lean recently and I don't have anything regarding Ito's formula. Regarding stochastic processes, we have the definition of martingales although a lot of the theories for it are for discrete martingales. I do think it is possible to define the Ito integral right now however.

[Josha Dekker]

Perhaps it is best to try to add something like the Lèvy-Ito formula (for general Lèvy processes) immediately to Mathlib, rather than just Ito. The former is much more general, it would be a pity if we wrote a lot of specialized API for Ito that doesn’t generalize well to a larger class of processes.