martingales

Stream: mathlib4

[Kevin Buzzard]

A statistician in my department asked me whether Lean has Continuous Time Martingales. He said that his understanding from reading the docs was that "only" discrete time Martingales have been implemented, but says he might be wrong. Can anyone clarify? Many thanks.

[Etienne Marion]

docs#MeasureTheory.Martingale is defined for an arbitrary preorder

[Rémy Degenne]

The definition is general, but all the meaningful results we have are about discrete time. So I'd say that "only discrete time" is a fair description of what we have right now.