Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 19:47 1ee91a5c

View on Github →

feat(probability_theory/stopping): define progressively measurable processes (#11350)

  • Define progressively measurable processes (prog_measurable), which is the correct strengthening of adapted to get that the stopped process is also progressively measurable.
  • Prove that an adapted continuous process is progressively measurable. For discrete time processes, progressively measurable is equivalent to adapted . This PR also changes some measurable_space arguments in measurable_space.lean from typeclass arguments to implicit.

Estimated changes

modified theorem measurable.prod_mk
modified theorem measurable.sum_elim
modified theorem measurable_fst
modified theorem measurable_inl
modified theorem measurable_inr
modified theorem measurable_prod
modified theorem measurable_snd
modified theorem measurable_sum
modified theorem measurable_swap
modified theorem measurable_swap_iff
modified theorem measurable_to_encodable
modified theorem measure_theory.adapted.add
modified theorem measure_theory.adapted.neg
modified theorem measure_theory.adapted.smul